The lion is rough. The mouse is nice. The squirrel needs the tiger. The tiger needs the mouse. If someone visits the tiger and they visit the mouse then they eat the mouse. If someone eats the tiger and they are kind then they eat the squirrel.
The lion is rough.
("lion" "is" "rough" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If someone visits the tiger and they visit the mouse then they eat the mouse.
((("someone" "visits" "tiger" "+") ("someone" "visits" "mouse" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the tiger and they are kind then they eat the squirrel.
((("someone" "eats" "tiger" "+") ("someone" "is" "kind" "+")) -> ("someone" "eats" "squirrel" "+"))
The squirrel needs the tiger.
True
1
proof
[(triple3)]
("squirrel" "needs" "tiger" "+")
triple3
The tiger does not need the mouse.
False
1
inv-proof
[(triple4)]
("tiger" "needs" "mouse" "-")
triple4
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel visits the tiger.
Unknown
random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "+")
@0: The lion is rough.[(triple1)] The mouse is nice.[(triple2)] The squirrel needs the tiger.[(triple3)] The tiger needs the mouse.[(triple4)]
The lion is rough.
("lion" "is" "rough" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple3
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple4