The squirrel eats the tiger. The squirrel likes the tiger. The squirrel needs the tiger. The tiger eats the squirrel. The tiger is big. The tiger likes the squirrel. The tiger needs the squirrel. If someone needs the tiger and the tiger likes the squirrel then they need the squirrel.
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If someone needs the tiger and the tiger likes the squirrel then they need the squirrel.
((("someone" "needs" "tiger" "+") ("tiger" "likes" "squirrel" "+")) -> ("someone" "needs" "squirrel" "+"))
The squirrel needs the tiger.
True
1
proof
[(triple3)]
("squirrel" "needs" "tiger" "+")
triple3
The tiger does not like the squirrel.
False
1
inv-proof
[(triple6)]
("tiger" "likes" "squirrel" "-")
triple6
The squirrel needs the squirrel.
True
3
proof
[(((triple3 triple6) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((triple3 triple6) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel does not need the squirrel.
False
3
inv-proof
[(((triple3 triple6) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((triple3 triple6) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The squirrel eats the tiger.[(triple1)] The squirrel likes the tiger.[(triple2)] The squirrel needs the tiger.[(triple3)] The tiger eats the squirrel.[(triple4)] The tiger is big.[(triple5)] The tiger likes the squirrel.[(triple6)] The tiger needs the squirrel.[(triple7)] @1: The squirrel needs the squirrel.[(((triple3 triple6) -> rule1))]
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple6
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple7
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple3 triple6) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1