The lion is cold. The lion likes the squirrel. The lion visits the squirrel. The squirrel is blue. The squirrel is cold. The squirrel is green. The squirrel is rough. The squirrel likes the lion. The squirrel needs the lion. The squirrel visits the lion. If something is green then it visits the squirrel. If something needs the lion then the lion is round.
The lion is cold.
("lion" "is" "cold" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something is green then it visits the squirrel.
((("something" "is" "green" "+")) -> ("something" "visits" "squirrel" "+"))
If something needs the lion then the lion is round.
((("something" "needs" "lion" "+")) -> ("lion" "is" "round" "+"))
The squirrel is cold.
True
1
proof
[(triple5)]
("squirrel" "is" "cold" "+")
triple5
The squirrel does not visit the lion.
False
1
inv-proof
[(triple10)]
("squirrel" "visits" "lion" "-")
triple10
The squirrel visits the squirrel.
True
2
proof
[(((triple6) -> rule1))]
("squirrel" "visits" "squirrel" "+")
((triple6) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple9) -> rule2))]
("lion" "is" "round" "-")
((triple9) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion does not need the squirrel.
Unknown
inv-random
[@0: The lion needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The lion is cold.[(triple1)] The lion likes the squirrel.[(triple2)] The lion visits the squirrel.[(triple3)] The squirrel is blue.[(triple4)] The squirrel is cold.[(triple5)] The squirrel is green.[(triple6)] The squirrel is rough.[(triple7)] The squirrel likes the lion.[(triple8)] The squirrel needs the lion.[(triple9)] The squirrel visits the lion.[(triple10)] @1: The lion is round.[(((triple9) -> rule2))] The squirrel visits the squirrel.[(((triple6) -> rule1))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple7
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple8
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple9
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple10
The lion is round.
("lion" "is" "round" "+")
((triple9) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple6) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1