The cat sees the mouse. The cow eats the mouse. The mouse likes the cow. The squirrel eats the cat. If someone sees the cat and the cat eats the squirrel then they see the cow. If the cat sees the cow and the cow likes the cat then the cat sees the mouse.
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
If someone sees the cat and the cat eats the squirrel then they see the cow.
((("someone" "sees" "cat" "+") ("cat" "eats" "squirrel" "+")) -> ("someone" "sees" "cow" "+"))
If the cat sees the cow and the cow likes the cat then the cat sees the mouse.
((("cat" "sees" "cow" "+") ("cow" "likes" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
The cow eats the mouse.
True
1
proof
[(triple2)]
("cow" "eats" "mouse" "+")
triple2
The squirrel does not eat the cat.
False
1
inv-proof
[(triple4)]
("squirrel" "eats" "cat" "-")
triple4
The cat does not see the cow.
Unknown
inv-rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cow" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat sees the mouse.[(triple1)] The cow eats the mouse.[(triple2)] The mouse likes the cow.[(triple3)] The squirrel eats the cat.[(triple4)]
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple3
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple4