The cat is nice. The cow needs the cat. The cow needs the mouse. The mouse needs the cat. The squirrel eats the cow. The squirrel is big. The squirrel likes the mouse. If someone eats the squirrel then the squirrel is cold. If someone likes the squirrel then they are cold. If the cat eats the cow then the cow likes the squirrel. If someone likes the mouse and the mouse likes the squirrel then they eat the cow. If someone is cold then they are nice. If someone likes the mouse then the mouse likes the squirrel.
The cat is nice.
("cat" "is" "nice" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If someone eats the squirrel then the squirrel is cold.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If someone likes the squirrel then they are cold.
((("someone" "likes" "squirrel" "+")) -> ("someone" "is" "cold" "+"))
If the cat eats the cow then the cow likes the squirrel.
((("cat" "eats" "cow" "+")) -> ("cow" "likes" "squirrel" "+"))
If someone likes the mouse and the mouse likes the squirrel then they eat the cow.
((("someone" "likes" "mouse" "+") ("mouse" "likes" "squirrel" "+")) -> ("someone" "eats" "cow" "+"))
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the mouse then the mouse likes the squirrel.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "squirrel" "+"))
The squirrel eats the cow.
True
1
proof
[(triple5 OR ((triple7 ((triple7) -> rule6)) -> rule4))]
("squirrel" "eats" "cow" "+")
triple5
((triple7 ((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The cow does not need the cat.
False
1
inv-proof
[(triple2)]
("cow" "needs" "cat" "-")
triple2
The mouse likes the squirrel.
True
2
proof
[(((triple7) -> rule6))]
("mouse" "likes" "squirrel" "+")
((triple7) -> (rule6 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse does not like the squirrel.
False
2
inv-proof
[(((triple7) -> rule6))]
("mouse" "likes" "squirrel" "-")
((triple7) -> (rule6 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse is cold.
True
3
proof
[(((((triple7) -> rule6)) -> rule2))]
("mouse" "is" "cold" "+")
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse is not cold.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule2))]
("mouse" "is" "cold" "-")
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse is nice.
True
4
proof
[(((((((triple7) -> rule6)) -> rule2)) -> rule5))]
("mouse" "is" "nice" "+")
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The mouse is not nice.
False
4
inv-proof
[(((((((triple7) -> rule6)) -> rule2)) -> rule5))]
("mouse" "is" "nice" "-")
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The cat does not eat the cow.
Unknown
inv-rconc
[@1: The cat eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "cow" "-")
The cow is cold.
Unknown
rconc
[@3: The cow is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule4 <- FAIL)]]
("cow" "is" "cold" "+")
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "cold" "-")
The cow eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cow" "+")
The mouse does not need the squirrel.
Unknown
inv-random
[@0: The mouse needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "squirrel" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is nice.[(triple1)] The cow needs the cat.[(triple2)] The cow needs the mouse.[(triple3)] The mouse needs the cat.[(triple4)] The squirrel eats the cow.[(triple5 OR ((triple7 ((triple7) -> rule6)) -> rule4))] The squirrel is big.[(triple6)] The squirrel likes the mouse.[(triple7)] @1: The mouse likes the squirrel.[(((triple7) -> rule6))] @2: The mouse is cold.[(((((triple7) -> rule6)) -> rule2))] @3: The mouse is nice.[(((((((triple7) -> rule6)) -> rule2)) -> rule5))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cow needs the cat.
("cow" "needs" "cat" "+")
triple2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple3
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple4
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple5
((triple7 ((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
triple6
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple7
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
((triple7) -> (rule6 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3