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