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