The lion is big. The lion is cold. The lion is rough. The lion is round. The lion likes the squirrel. The lion needs the squirrel. The lion sees the squirrel. The squirrel is big. The squirrel is green. The squirrel likes the lion. The squirrel needs the lion. The squirrel sees the lion. If something sees the squirrel then it sees the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If something sees the squirrel then it sees the lion.
((("something" "sees" "squirrel" "+")) -> ("something" "sees" "lion" "+"))
The squirrel sees the lion.
True
1
proof
[(triple12)]
("squirrel" "sees" "lion" "+")
triple12
The lion is not cold.
False
1
inv-proof
[(triple2)]
("lion" "is" "cold" "-")
triple2
The lion sees the lion.
True
2
proof
[(((triple7) -> rule1))]
("lion" "sees" "lion" "+")
((triple7) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple7) -> rule1))]
("lion" "sees" "lion" "-")
((triple7) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
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 squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The lion is big.[(triple1)] The lion is cold.[(triple2)] The lion is rough.[(triple3)] The lion is round.[(triple4)] The lion likes the squirrel.[(triple5)] The lion needs the squirrel.[(triple6)] The lion sees the squirrel.[(triple7)] The squirrel is big.[(triple8)] The squirrel is green.[(triple9)] The squirrel likes the lion.[(triple10)] The squirrel needs the lion.[(triple11)] The squirrel sees the lion.[(triple12)] @1: The lion sees the lion.[(((triple7) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple5
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple6
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple9
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple10
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple11
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple12
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple7) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1