The lion is round. The mouse needs the squirrel. The squirrel sees the mouse. If something sees the lion and it is not nice then it likes the mouse. If the lion is round then the lion is rough. If something likes the squirrel then the squirrel needs the lion. If something is nice then it needs the squirrel. If something is nice and not round then it needs the mouse. If something likes the lion and it needs the squirrel then the lion needs the mouse.
The lion is round.
("lion" "is" "round" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If something sees the lion and it is not nice then it likes the mouse.
((("something" "sees" "lion" "+") ("something" "is" "nice" "~")) -> ("something" "likes" "mouse" "+"))
If the lion is round then the lion is rough.
((("lion" "is" "round" "+")) -> ("lion" "is" "rough" "+"))
If something likes the squirrel then the squirrel needs the lion.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "needs" "lion" "+"))
If something is nice then it needs the squirrel.
((("something" "is" "nice" "+")) -> ("something" "needs" "squirrel" "+"))
If something is nice and not round then it needs the mouse.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "needs" "mouse" "+"))
If something likes the lion and it needs the squirrel then the lion needs the mouse.
((("something" "likes" "lion" "+") ("something" "needs" "squirrel" "+")) -> ("lion" "needs" "mouse" "+"))
The squirrel sees the mouse.
True
1
proof
[(triple3)]
("squirrel" "sees" "mouse" "+")
triple3
The squirrel does not see the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "sees" "mouse" "-")
triple3
The lion is rough.
True
2
proof
[(((triple1) -> rule2))]
("lion" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("lion" "is" "rough" "-")
((triple1) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The squirrel needs the squirrel.
Unknown
rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "squirrel" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The lion is round.[(triple1)] The mouse needs the squirrel.[(triple2)] The squirrel sees the mouse.[(triple3)] @1: The lion is rough.[(((triple1) -> rule2))]
The lion is round.
("lion" "is" "round" "+")
triple1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1