The cat visits the squirrel. The mouse likes the squirrel. The squirrel eats the mouse. If the cat visits the squirrel then the squirrel visits the cat. If someone is kind and they visit the squirrel then they like the mouse. If someone is blue and they like the cat then they eat the squirrel.
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
If the cat visits the squirrel then the squirrel visits the cat.
((("cat" "visits" "squirrel" "+")) -> ("squirrel" "visits" "cat" "+"))
If someone is kind and they visit the squirrel then they like the mouse.
((("someone" "is" "kind" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is blue and they like the cat then they eat the squirrel.
((("someone" "is" "blue" "+") ("someone" "likes" "cat" "+")) -> ("someone" "eats" "squirrel" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple3)]
("squirrel" "eats" "mouse" "+")
triple3
The squirrel does not eat the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "mouse" "-")
triple3
The cat does not like the mouse.
Unknown
inv-rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "mouse" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat visits the squirrel.[(triple1)] The mouse likes the squirrel.[(triple2)] The squirrel eats the mouse.[(triple3)] @1: The squirrel visits the cat.[(((triple1) -> rule1))]
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple1) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1