The cat eats the squirrel. The cow eats the cat. The squirrel is rough. The tiger is red. If the tiger is cold and the tiger visits the cow then the tiger is green. If the cat needs the tiger and the tiger needs the squirrel then the cat needs the cow.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The tiger is red.
("tiger" "is" "red" "+")
If the tiger is cold and the tiger visits the cow then the tiger is green.
((("tiger" "is" "cold" "+") ("tiger" "visits" "cow" "+")) -> ("tiger" "is" "green" "+"))
If the cat needs the tiger and the tiger needs the squirrel then the cat needs the cow.
((("cat" "needs" "tiger" "+") ("tiger" "needs" "squirrel" "+")) -> ("cat" "needs" "cow" "+"))
The cat eats the squirrel.
True
1
proof
[(triple1)]
("cat" "eats" "squirrel" "+")
triple1
The tiger is not red.
False
1
inv-proof
[(triple4)]
("tiger" "is" "red" "-")
triple4
The tiger is not green.
Unknown
inv-rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "green" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The cat eats the squirrel.[(triple1)] The cow eats the cat.[(triple2)] The squirrel is rough.[(triple3)] The tiger is red.[(triple4)]
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The cow eats the cat.
("cow" "eats" "cat" "+")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4