/****************************************************************
* This file is part of CLKR - www.fernuni-hagen.de/wbs/clkr/
* 
* File       : ex0004_birds004.cl
* Type       : KB
* Domain     : Examples
* Date       : 2023-12-19
* Version    : v1.0
* 
* Details    : Signature size        : 4
*              #Knowledge Bases      : 4
*              #Conditionals per KB  : 3 - 5
* 
* Refs       : 
*
* Comments   : Counter Example for proposition that conditionals are redundant iff there is a solution of CR(R) with impact 0: r2 and r3 have 
*              solutions with impact 0; nither r2 nor r3 are redundant in birds004
*
****************************************************************/

signature
   p,b,s,f

conditionals
birds004{
   (b | p),      // r1
   (b | !p),     // r2
   (b | !p,s,f), // r3
   (s | !b,f),   // r4
   (p | !f)      // r5
}
birds004_minus_r2{   // does not entail r2 (p-Inference)
   (b | p),
   (b | !p,s,f),
   (s | !b,f),
   (p | !f)
}
birds004_minus_r3{   // does not entail r3 (p-Inference)
   (b | p),
   (b | !p),
   (s | !b,f),
   (p | !f)
}
min_example{
   (b | p),   // r1
   (b | !p),  // r2
   (b | !p,s) // r3  has solutions with impact 0
}