The lion is kind. The lion is round. The lion likes the mouse. The lion needs the squirrel. The mouse chases the squirrel. The mouse is round. The squirrel is kind. If someone chases the lion then the lion chases the mouse. If someone likes the mouse then the mouse needs the lion.
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is round.
("mouse" "is" "round" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If someone chases the lion then the lion chases the mouse.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "mouse" "+"))
If someone likes the mouse then the mouse needs the lion.
((("someone" "likes" "mouse" "+")) -> ("mouse" "needs" "lion" "+"))
The lion likes the mouse.
True
1
proof
[(triple3)]
("lion" "likes" "mouse" "+")
triple3
The lion does not like the mouse.
False
1
inv-proof
[(triple3)]
("lion" "likes" "mouse" "-")
triple3
The mouse needs the lion.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "needs" "lion" "+")
((triple3) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse does not need the lion.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "needs" "lion" "-")
((triple3) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion does not chase the mouse.
Unknown
inv-rconc
[@1: The lion chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "mouse" "-")
The lion needs the mouse.
Unknown
random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "+")
The squirrel does not like the mouse.
Unknown
inv-random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "-")
The squirrel needs the lion.
Unknown
random
[@0: The squirrel needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "lion" "+")
@0: The lion is kind.[(triple1)] The lion is round.[(triple2)] The lion likes the mouse.[(triple3)] The lion needs the squirrel.[(triple4)] The mouse chases the squirrel.[(triple5)] The mouse is round.[(triple6)] The squirrel is kind.[(triple7)] @1: The mouse needs the lion.[(((triple3) -> rule2))]
The lion is kind.
("lion" "is" "kind" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple4
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple7
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple3) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1