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