The cat sees the rabbit. The rabbit is big. The squirrel sees the rabbit. The tiger sees the rabbit. If someone sees the cat then the cat eats the squirrel. If someone visits the squirrel and the squirrel is cold then the squirrel eats the cat. If someone visits the tiger then they are not big. If someone visits the tiger then they visit the rabbit. If someone visits the squirrel and they are not red then the squirrel is rough. If someone is red and they do not eat the tiger then the tiger does not eat the cat. If someone is red then they do not visit the tiger. If someone is cold and not big then they do not eat the rabbit.
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone sees the cat then the cat eats the squirrel.
((("someone" "sees" "cat" "+")) -> ("cat" "eats" "squirrel" "+"))
If someone visits the squirrel and the squirrel is cold then the squirrel eats the cat.
((("someone" "visits" "squirrel" "+") ("squirrel" "is" "cold" "+")) -> ("squirrel" "eats" "cat" "+"))
If someone visits the tiger then they are not big.
((("someone" "visits" "tiger" "+")) -> ("someone" "is" "big" "-"))
If someone visits the tiger then they visit the rabbit.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the squirrel and they are not red then the squirrel is rough.
((("someone" "visits" "squirrel" "+") ("someone" "is" "red" "~")) -> ("squirrel" "is" "rough" "+"))
If someone is red and they do not eat the tiger then the tiger does not eat the cat.
((("someone" "is" "red" "+") ("someone" "eats" "tiger" "~")) -> ("tiger" "eats" "cat" "-"))
If someone is red then they do not visit the tiger.
((("someone" "is" "red" "+")) -> ("someone" "visits" "tiger" "-"))
If someone is cold and not big then they do not eat the rabbit.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "eats" "rabbit" "-"))
The rabbit is big.
True
1
proof
[(triple2)]
("rabbit" "is" "big" "+")
triple2
The squirrel does not see the rabbit.
False
1
inv-proof
[(triple3)]
("squirrel" "sees" "rabbit" "-")
triple3
The squirrel does not eat the cat.
Unknown
inv-rconc
[@1: The squirrel eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat sees the rabbit.[(triple1)] The rabbit is big.[(triple2)] The squirrel sees the rabbit.[(triple3)] The tiger sees the rabbit.[(triple4)]
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple4