The lion is big. The lion is blue. The lion is not cold. The lion is green. The lion needs the squirrel. The lion sees the squirrel. The lion visits the squirrel. The squirrel is green. The squirrel is not red. The squirrel needs the lion. The squirrel sees the lion. The squirrel visits the lion. If someone is green then they need the squirrel. If someone visits the lion and they see the squirrel then the squirrel does not visit the lion. If the squirrel needs the lion then the squirrel is green.
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The lion is green.
("lion" "is" "green" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is not red.
("squirrel" "is" "red" "-")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If someone is green then they need the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone visits the lion and they see the squirrel then the squirrel does not visit the lion.
((("someone" "visits" "lion" "+") ("someone" "sees" "squirrel" "+")) -> ("squirrel" "visits" "lion" "-"))
If the squirrel needs the lion then the squirrel is green.
((("squirrel" "needs" "lion" "+")) -> ("squirrel" "is" "green" "+"))
The squirrel sees the lion.
True
1
proof
[(triple11)]
("squirrel" "sees" "lion" "+")
triple11
The lion does not visit the squirrel.
False
1
inv-proof
[(triple7)]
("lion" "visits" "squirrel" "-")
triple7
The squirrel needs the squirrel.
True
2
proof
[(((triple8) -> rule1) OR ((((triple10) -> rule3)) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((triple8) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not need the squirrel.
False
2
inv-proof
[(((triple8) -> rule1) OR ((((triple10) -> rule3)) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((triple8) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The lion is big.[(triple1)] The lion is blue.[(triple2)] The lion is green.[(triple4)] The lion is not cold.[(triple3)] The lion needs the squirrel.[(triple5 OR ((triple4) -> rule1))] The lion sees the squirrel.[(triple6)] The lion visits the squirrel.[(triple7)] The squirrel is green.[(triple8 OR ((triple10) -> rule3))] The squirrel is not red.[(triple9)] The squirrel needs the lion.[(triple10)] The squirrel sees the lion.[(triple11)] The squirrel visits the lion.[(triple12)] @1: The squirrel needs the squirrel.[(((triple8) -> rule1) OR ((((triple10) -> rule3)) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple4
The lion is not cold.
("lion" "is" "cold" "-")
triple3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple5
((triple4) -> (rule1 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple6
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
((triple10) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not red.
("squirrel" "is" "red" "-")
triple9
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple10
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple11
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple12
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple8) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2