The squirrel chases the tiger. The squirrel is not big. The squirrel is kind. The squirrel is nice. The squirrel is rough. The squirrel is round. The squirrel needs the tiger. The squirrel sees the tiger. The tiger chases the squirrel. The tiger is big. The tiger is kind. The tiger is not nice. The tiger is round. The tiger needs the squirrel. The tiger does not see the squirrel. If something needs the tiger then the tiger chases the squirrel. If something needs the squirrel then the squirrel is rough.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
If something needs the tiger then the tiger chases the squirrel.
((("something" "needs" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
If something needs the squirrel then the squirrel is rough.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
The squirrel is nice.
True
1
proof
[(triple4)]
("squirrel" "is" "nice" "+")
triple4
The squirrel does not see the tiger.
False
1
inv-proof
[(triple8)]
("squirrel" "sees" "tiger" "-")
triple8
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
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 kind.[(triple3)] The squirrel is nice.[(triple4)] The squirrel is not big.[(triple2)] The squirrel is rough.[(triple5 OR ((triple14) -> rule2))] The squirrel is round.[(triple6)] The squirrel needs the tiger.[(triple7)] The squirrel sees the tiger.[(triple8)] The tiger chases the squirrel.[(triple9 OR ((triple7) -> rule1))] The tiger does not see the squirrel.[(triple15)] The tiger is big.[(triple10)] The tiger is kind.[(triple11)] The tiger is not nice.[(triple12)] The tiger is round.[(triple13)] The tiger needs the squirrel.[(triple14)]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple4
The squirrel is not big.
("squirrel" "is" "big" "-")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple5
((triple14) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
triple6
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple7
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple8
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple9
((triple7) -> (rule1 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
triple15
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is not nice.
("tiger" "is" "nice" "-")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple14