The cat is nice. The cow visits the squirrel. The mouse visits the squirrel. The squirrel needs the mouse. If someone is nice then they need the squirrel. If someone is big and nice then they need the mouse. If someone likes the squirrel then they do not need the mouse. If someone needs the squirrel then they like the cow. If someone likes the cow then they like the mouse. If the cat is big and the cat is nice then the cat visits the cow. If someone likes the cow and they are round then they need the cat. If someone is blue and they like the cat then they are big.
The cat is nice.
("cat" "is" "nice" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If someone is nice then they need the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone is big and nice then they need the mouse.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "mouse" "+"))
If someone likes the squirrel then they do not need the mouse.
((("someone" "likes" "squirrel" "+")) -> ("someone" "needs" "mouse" "-"))
If someone needs the squirrel then they like the cow.
((("someone" "needs" "squirrel" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow then they like the mouse.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "mouse" "+"))
If the cat is big and the cat is nice then the cat visits the cow.
((("cat" "is" "big" "+") ("cat" "is" "nice" "+")) -> ("cat" "visits" "cow" "+"))
If someone likes the cow and they are round then they need the cat.
((("someone" "likes" "cow" "+") ("someone" "is" "round" "+")) -> ("someone" "needs" "cat" "+"))
If someone is blue and they like the cat then they are big.
((("someone" "is" "blue" "+") ("someone" "likes" "cat" "+")) -> ("someone" "is" "big" "+"))
The cow visits the squirrel.
True
1
proof
[(triple2)]
("cow" "visits" "squirrel" "+")
triple2
The squirrel does not need the mouse.
False
1
inv-proof
[(triple4)]
("squirrel" "needs" "mouse" "-")
triple4
The cat needs the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("cat" "needs" "squirrel" "+")
((triple1) -> (rule1 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cat does not need the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "needs" "squirrel" "-")
((triple1) -> (rule1 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cat likes the cow.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("cat" "likes" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int2
The cat does not like the cow.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("cat" "likes" "cow" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int2
The cat does not need the mouse.
Unknown
inv-rconc
[@2: The cat needs the mouse.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("cat" "needs" "mouse" "-")
The mouse likes the cow.
Unknown
rconc
[@2: The mouse likes the cow.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("mouse" "likes" "cow" "+")
The squirrel does not like the mouse.
Unknown
inv-rconc
[@3: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("squirrel" "likes" "mouse" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The mouse does not like the cat.
Unknown
inv-random
[@0: The mouse likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cat" "-")
The squirrel visits the cat.
Unknown
random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "+")
@0: The cat is nice.[(triple1)] The cow visits the squirrel.[(triple2)] The mouse visits the squirrel.[(triple3)] The squirrel needs the mouse.[(triple4)] @1: The cat needs the squirrel.[(((triple1) -> rule1))] @2: The cat likes the cow.[(((((triple1) -> rule1)) -> rule4))] @3: The cat likes the mouse.[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple3
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple4
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
((triple1) -> (rule1 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int3