The lion eats the mouse. The mouse eats the lion. The squirrel needs the mouse. If the lion eats the mouse then the mouse needs the lion. If someone is round then they eat the mouse.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If the lion eats the mouse then the mouse needs the lion.
((("lion" "eats" "mouse" "+")) -> ("mouse" "needs" "lion" "+"))
If someone is round then they eat the mouse.
((("someone" "is" "round" "+")) -> ("someone" "eats" "mouse" "+"))
The squirrel needs the mouse.
True
1
proof
[(triple3)]
("squirrel" "needs" "mouse" "+")
triple3
The mouse does not eat the lion.
False
1
inv-proof
[(triple2)]
("mouse" "eats" "lion" "-")
triple2
The mouse needs the lion.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "needs" "lion" "+")
((triple1) -> (rule1 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse does not need the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "needs" "lion" "-")
((triple1) -> (rule1 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The squirrel eats the mouse.
Unknown
rconc
[@1: The squirrel eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "mouse" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The squirrel visits the mouse.
Unknown
random
[@0: The squirrel visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "mouse" "+")
@0: The lion eats the mouse.[(triple1)] The mouse eats the lion.[(triple2)] The squirrel needs the mouse.[(triple3)] @1: The mouse needs the lion.[(((triple1) -> rule1))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple3
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple1) -> (rule1 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1