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