The squirrel chases the tiger. The squirrel is big. The squirrel is kind. The squirrel is not red. The squirrel is round. The squirrel does not need the tiger. The squirrel visits the tiger. The tiger chases the squirrel. The tiger is not big. The tiger is kind. The tiger is red. The tiger is round. The tiger is young. The tiger does not need the squirrel. The tiger visits the squirrel. If someone chases the tiger then they need the squirrel. If someone needs the squirrel then they are young.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is not red.
("squirrel" "is" "red" "-")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone chases the tiger then they need the squirrel.
((("someone" "chases" "tiger" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone needs the squirrel then they are young.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "young" "+"))
The tiger is not big.
True
1
proof
[(triple9)]
("tiger" "is" "big" "-")
triple9
The squirrel does not visit the tiger.
False
1
inv-proof
[(triple7)]
("squirrel" "visits" "tiger" "-")
triple7
The squirrel needs the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((triple1) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel does not need the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((triple1) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is young.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("squirrel" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is not young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("squirrel" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
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 does not need the tiger.[(triple6)] The squirrel is big.[(triple2)] The squirrel is kind.[(triple3)] The squirrel is not red.[(triple4)] The squirrel is round.[(triple5)] The squirrel visits the tiger.[(triple7)] The tiger chases the squirrel.[(triple8)] The tiger does not need the squirrel.[(triple14)] The tiger is kind.[(triple10)] The tiger is not big.[(triple9)] The tiger is red.[(triple11)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger visits the squirrel.[(triple15)] @1: The squirrel needs the squirrel.[(((triple1) -> rule1))] @2: The squirrel is young.[(((((triple1) -> rule1)) -> rule2))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The squirrel is not red.
("squirrel" "is" "red" "-")
triple4
The squirrel is round.
("squirrel" "is" "round" "+")
triple5
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple8
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple14
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is not big.
("tiger" "is" "big" "-")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple15
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple1) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2