The cow eats the squirrel. The cow is big. The cow is cold. The cow is round. The cow needs the mouse. The cow needs the squirrel. The mouse eats the squirrel. The mouse is cold. The mouse is red. The mouse needs the cow. The mouse needs the squirrel. The rabbit needs the cow. The squirrel eats the cow. The squirrel likes the cow. The squirrel likes the rabbit. The squirrel needs the mouse. If something eats the squirrel then the squirrel is cold. If something needs the rabbit and the rabbit is big then it is big. If something eats the cow and the cow likes the rabbit then the rabbit likes the squirrel. If the mouse likes the rabbit and the rabbit is big then the rabbit needs the squirrel. If something likes the cow and the cow is nice then the cow likes the mouse. If the cow is red then the cow is nice. If something needs the mouse then it is red. If something is nice and it needs the squirrel then it is cold.
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something eats the squirrel then the squirrel is cold.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If something needs the rabbit and the rabbit is big then it is big.
((("something" "needs" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("something" "is" "big" "+"))
If something eats the cow and the cow likes the rabbit then the rabbit likes the squirrel.
((("something" "eats" "cow" "+") ("cow" "likes" "rabbit" "+")) -> ("rabbit" "likes" "squirrel" "+"))
If the mouse likes the rabbit and the rabbit is big then the rabbit needs the squirrel.
((("mouse" "likes" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If something likes the cow and the cow is nice then the cow likes the mouse.
((("something" "likes" "cow" "+") ("cow" "is" "nice" "+")) -> ("cow" "likes" "mouse" "+"))
If the cow is red then the cow is nice.
((("cow" "is" "red" "+")) -> ("cow" "is" "nice" "+"))
If something needs the mouse then it is red.
((("something" "needs" "mouse" "+")) -> ("something" "is" "red" "+"))
If something is nice and it needs the squirrel then it is cold.
((("something" "is" "nice" "+") ("something" "needs" "squirrel" "+")) -> ("something" "is" "cold" "+"))
The squirrel eats the cow.
True
1
proof
[(triple13)]
("squirrel" "eats" "cow" "+")
triple13
The cow does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "eats" "squirrel" "-")
triple1
The squirrel is cold.
True
2
proof
[(((triple1) -> rule1) OR ((triple7) -> rule1))]
("squirrel" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((triple7) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple5) -> rule7))]
("cow" "is" "red" "-")
((triple5) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is nice.
True
3
proof
[(((((triple5) -> rule7)) -> rule6))]
("cow" "is" "nice" "+")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is not nice.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule6))]
("cow" "is" "nice" "-")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the mouse.
True
5
proof
[(((triple14 ((((triple5) -> rule7)) -> rule6)) -> rule5))]
("cow" "likes" "mouse" "+")
((triple14 ((((triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow does not like the mouse.
False
5
inv-proof
[(((triple14 ((((triple5) -> rule7)) -> rule6)) -> rule5))]
("cow" "likes" "mouse" "-")
((triple14 ((((triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The rabbit is not cold.
Unknown
inv-rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "cold" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "big" "+")
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "big" "+")
The rabbit does not eat the squirrel.
Unknown
inv-random
[@0: The rabbit eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "squirrel" "-")
The squirrel eats the mouse.
Unknown
random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "+")
The rabbit does not eat the cow.
Unknown
inv-random
[@0: The rabbit eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cow" "-")
The squirrel needs the cow.
Unknown
random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "+")
@0: The cow eats the squirrel.[(triple1)] The cow is big.[(triple2)] The cow is cold.[(triple3 OR ((((((triple5) -> rule7)) -> rule6) triple6) -> rule8))] The cow is round.[(triple4)] The cow needs the mouse.[(triple5)] The cow needs the squirrel.[(triple6)] The mouse eats the squirrel.[(triple7)] The mouse is cold.[(triple8)] The mouse is red.[(triple9)] The mouse needs the cow.[(triple10)] The mouse needs the squirrel.[(triple11)] The rabbit needs the cow.[(triple12)] The squirrel eats the cow.[(triple13)] The squirrel likes the cow.[(triple14)] The squirrel likes the rabbit.[(triple15)] The squirrel needs the mouse.[(triple16)] @1: The cow is red.[(((triple5) -> rule7))] The squirrel is cold.[(((triple1) -> rule1) OR ((triple7) -> rule1))] The squirrel is red.[(((triple16) -> rule7))] @2: The cow is nice.[(((((triple5) -> rule7)) -> rule6))] @3: The cow likes the mouse.[(((triple14 ((((triple5) -> rule7)) -> rule6)) -> rule5))]
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2)) triple6) -> (rule8 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple6
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse is red.
("mouse" "is" "red" "+")
triple9
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple10
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple11
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple12
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple13
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple14
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple15
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple16
The cow is red.
("cow" "is" "red" "+")
((triple5) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((triple7) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((triple16) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((triple14 ((((triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3