The lion chases the squirrel. The lion is big. The lion is not blue. The lion is cold. The lion is red. The lion is not young. The lion likes the squirrel. The lion visits the squirrel. The squirrel is not big. The squirrel likes the lion. If someone chases the squirrel then the squirrel is not red.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is not blue.
("lion" "is" "blue" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
If someone chases the squirrel then the squirrel is not red.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "red" "-"))
The lion is big.
True
1
proof
[(triple2)]
("lion" "is" "big" "+")
triple2
The lion is blue.
False
1
inv-proof
[(triple3)]
("lion" "is" "blue" "+")
triple3
The squirrel is not red.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "is" "red" "-")
((triple1) -> (rule1 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is red.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "is" "red" "+")
((triple1) -> (rule1 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The lion chases the squirrel.[(triple1)] The lion is big.[(triple2)] The lion is cold.[(triple4)] The lion is not blue.[(triple3)] The lion is not young.[(triple6)] The lion is red.[(triple5)] The lion likes the squirrel.[(triple7)] The lion visits the squirrel.[(triple8)] The squirrel is not big.[(triple9)] The squirrel likes the lion.[(triple10)] @1: The squirrel is not red.[(((triple1) -> rule1))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is not blue.
("lion" "is" "blue" "-")
triple3
The lion is not young.
("lion" "is" "young" "-")
triple6
The lion is red.
("lion" "is" "red" "+")
triple5
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple7
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple8
The squirrel is not big.
("squirrel" "is" "big" "-")
triple9
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple10
The squirrel is not red.
("squirrel" "is" "red" "-")
((triple1) -> (rule1 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1