The lion eats the squirrel. The lion is not big. The lion is cold. The lion is red. The lion is round. The lion is young. The lion sees the squirrel. The lion visits the squirrel. The squirrel eats the lion. The squirrel is big. The squirrel is cold. The squirrel is red. The squirrel is round. The squirrel is young. The squirrel sees the lion. The squirrel visits the lion. If the squirrel is not red then the squirrel is big. If something visits the squirrel then it is young.
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If the squirrel is not red then the squirrel is big.
((("squirrel" "is" "red" "~")) -> ("squirrel" "is" "big" "+"))
If something visits the squirrel then it is young.
((("something" "visits" "squirrel" "+")) -> ("something" "is" "young" "+"))
The squirrel is big.
True
1
proof
[(triple10)]
("squirrel" "is" "big" "+")
triple10
The squirrel does not see the lion.
False
1
inv-proof
[(triple15)]
("squirrel" "sees" "lion" "-")
triple15
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The lion eats the squirrel.[(triple1)] The lion is cold.[(triple3)] The lion is not big.[(triple2)] The lion is red.[(triple4)] The lion is round.[(triple5)] The lion is young.[(triple6 OR ((triple8) -> rule2))] The lion sees the squirrel.[(triple7)] The lion visits the squirrel.[(triple8)] The squirrel eats the lion.[(triple9)] The squirrel is big.[(triple10)] The squirrel is cold.[(triple11)] The squirrel is red.[(triple12)] The squirrel is round.[(triple13)] The squirrel is young.[(triple14)] The squirrel sees the lion.[(triple15)] The squirrel visits the lion.[(triple16)]
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is not big.
("lion" "is" "big" "-")
triple2
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
((triple8) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple7
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple8
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple9
The squirrel is big.
("squirrel" "is" "big" "+")
triple10
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple11
The squirrel is red.
("squirrel" "is" "red" "+")
triple12
The squirrel is round.
("squirrel" "is" "round" "+")
triple13
The squirrel is young.
("squirrel" "is" "young" "+")
triple14
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple15
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple16