The squirrel eats the tiger. The squirrel is blue. The squirrel is green. The squirrel is kind. The squirrel is young. The squirrel sees the tiger. The squirrel visits the tiger. The tiger eats the squirrel. The tiger is blue. The tiger is kind. The tiger is young. The tiger sees the squirrel. If something visits the tiger then the tiger visits the squirrel. If something sees the squirrel and the squirrel is green then it is green.
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something visits the tiger then the tiger visits the squirrel.
((("something" "visits" "tiger" "+")) -> ("tiger" "visits" "squirrel" "+"))
If something sees the squirrel and the squirrel is green then it is green.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "green" "+")) -> ("something" "is" "green" "+"))
The squirrel is green.
True
1
proof
[(triple3)]
("squirrel" "is" "green" "+")
triple3
The squirrel does not eat the tiger.
False
1
inv-proof
[(triple1)]
("squirrel" "eats" "tiger" "-")
triple1
The tiger visits the squirrel.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "visits" "squirrel" "+")
((triple7) -> (rule1 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is not green.
False
3
inv-proof
[(((triple12 triple3) -> rule2))]
("tiger" "is" "green" "-")
((triple12 triple3) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
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 tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The squirrel eats the tiger.[(triple1)] The squirrel is blue.[(triple2)] The squirrel is green.[(triple3)] The squirrel is kind.[(triple4)] The squirrel is young.[(triple5)] The squirrel sees the tiger.[(triple6)] The squirrel visits the tiger.[(triple7)] The tiger eats the squirrel.[(triple8)] The tiger is blue.[(triple9)] The tiger is kind.[(triple10)] The tiger is young.[(triple11)] The tiger sees the squirrel.[(triple12)] @1: The tiger is green.[(((triple12 triple3) -> rule2))] The tiger visits the squirrel.[(((triple7) -> rule1))]
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The squirrel is green.
("squirrel" "is" "green" "+")
triple3
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple4
The squirrel is young.
("squirrel" "is" "young" "+")
triple5
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple6
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple7
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
triple11
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
((triple12 triple3) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((triple7) -> (rule1 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1