The lion is big. The lion is blue. The lion sees the squirrel. The lion visits the rabbit. The lion visits the squirrel. The rabbit is blue. The rabbit needs the lion. The rabbit needs the squirrel. The rabbit sees the squirrel. The squirrel is blue. The squirrel is green. The squirrel is rough. The squirrel needs the rabbit. The squirrel sees the lion. The squirrel sees the rabbit. The squirrel visits the lion. If something needs the rabbit then the rabbit sees the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something needs the rabbit then the rabbit sees the lion.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
The squirrel is green.
True
1
proof
[(triple11)]
("squirrel" "is" "green" "+")
triple11
The lion does not visit the squirrel.
False
1
inv-proof
[(triple5)]
("lion" "visits" "squirrel" "-")
triple5
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The lion sees the rabbit.
Unknown
random
[@0: The lion sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "rabbit" "+")
@0: The lion is big.[(triple1)] The lion is blue.[(triple2)] The lion sees the squirrel.[(triple3)] The lion visits the rabbit.[(triple4)] The lion visits the squirrel.[(triple5)] The rabbit is blue.[(triple6)] The rabbit needs the lion.[(triple7)] The rabbit needs the squirrel.[(triple8)] The rabbit sees the squirrel.[(triple9)] The squirrel is blue.[(triple10)] The squirrel is green.[(triple11)] The squirrel is rough.[(triple12)] The squirrel needs the rabbit.[(triple13)] The squirrel sees the lion.[(triple14)] The squirrel sees the rabbit.[(triple15)] The squirrel visits the lion.[(triple16)] @1: The rabbit sees the lion.[(((triple13) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple3
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple4
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple5
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple6
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple7
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple8
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel is green.
("squirrel" "is" "green" "+")
triple11
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple12
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple13
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple14
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple15
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple16
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((triple13) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1