The squirrel chases the tiger. The squirrel is big. The squirrel is red. The squirrel is young. The squirrel needs the tiger. The squirrel visits the tiger. The tiger is green. The tiger is red. The tiger needs the squirrel. The tiger visits the squirrel. If something is big then it visits the squirrel.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something is big then it visits the squirrel.
((("something" "is" "big" "+")) -> ("something" "visits" "squirrel" "+"))
The tiger is red.
True
1
proof
[(triple8)]
("tiger" "is" "red" "+")
triple8
The squirrel does not visit the tiger.
False
1
inv-proof
[(triple6)]
("squirrel" "visits" "tiger" "-")
triple6
The squirrel visits the squirrel.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "visits" "squirrel" "+")
((triple2) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "visits" "squirrel" "-")
((triple2) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The squirrel chases the tiger.[(triple1)] The squirrel is big.[(triple2)] The squirrel is red.[(triple3)] The squirrel is young.[(triple4)] The squirrel needs the tiger.[(triple5)] The squirrel visits the tiger.[(triple6)] The tiger is green.[(triple7)] The tiger is red.[(triple8)] The tiger needs the squirrel.[(triple9)] The tiger visits the squirrel.[(triple10)] @1: The squirrel visits the squirrel.[(((triple2) -> rule1))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The squirrel is big.
("squirrel" "is" "big" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple5
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple9
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple10
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple2) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1