The cat needs the rabbit. The mouse needs the tiger. The rabbit likes the cat. The tiger eats the rabbit. If someone likes the tiger and the tiger eats the mouse then they need the mouse. If someone is blue then they like the tiger.
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
If someone likes the tiger and the tiger eats the mouse then they need the mouse.
((("someone" "likes" "tiger" "+") ("tiger" "eats" "mouse" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is blue then they like the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "tiger" "+"))
The mouse needs the tiger.
True
1
proof
[(triple2)]
("mouse" "needs" "tiger" "+")
triple2
The rabbit does not like the cat.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "cat" "-")
triple3
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "mouse" "-")
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 needs the rabbit.[(triple1)] The mouse needs the tiger.[(triple2)] The rabbit likes the cat.[(triple3)] The tiger eats the rabbit.[(triple4)]
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple2
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple3
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple4