The cow needs the squirrel. The cow sees the squirrel. The squirrel eats the cow. The squirrel is green. The squirrel needs the tiger. The squirrel sees the cow. The tiger eats the squirrel. The tiger is green. The tiger is round. The tiger sees the squirrel. If something sees the cow then it eats the cow. If something sees the squirrel and it is green then the squirrel eats the tiger. If something sees the squirrel then it eats the tiger. If something eats the tiger then the tiger sees the cow. If something eats the tiger then it sees the cow. If something needs the tiger then the tiger is big.
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something sees the cow then it eats the cow.
((("something" "sees" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something sees the squirrel and it is green then the squirrel eats the tiger.
((("something" "sees" "squirrel" "+") ("something" "is" "green" "+")) -> ("squirrel" "eats" "tiger" "+"))
If something sees the squirrel then it eats the tiger.
((("something" "sees" "squirrel" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the tiger then the tiger sees the cow.
((("something" "eats" "tiger" "+")) -> ("tiger" "sees" "cow" "+"))
If something eats the tiger then it sees the cow.
((("something" "eats" "tiger" "+")) -> ("something" "sees" "cow" "+"))
If something needs the tiger then the tiger is big.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "big" "+"))
The tiger eats the squirrel.
True
1
proof
[(triple7)]
("tiger" "eats" "squirrel" "+")
triple7
The tiger is not round.
False
1
inv-proof
[(triple9)]
("tiger" "is" "round" "-")
triple9
The cow eats the tiger.
True
2
proof
[(((triple2) -> rule3))]
("cow" "eats" "tiger" "+")
((triple2) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The tiger is not big.
False
2
inv-proof
[(((triple5) -> rule6))]
("tiger" "is" "big" "-")
((triple5) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger sees the cow.
True
3
proof
[(((((triple10) -> rule3)) -> rule4) OR ((((triple10) -> rule3)) -> rule5) OR ((((triple2) -> rule3)) -> rule4) OR ((((triple10 triple8) -> rule2)) -> rule4))]
("tiger" "sees" "cow" "+")
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
((((triple10 triple8) -> (rule2 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The tiger does not see the cow.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule4) OR ((((triple10) -> rule3)) -> rule5) OR ((((triple2) -> rule3)) -> rule4) OR ((((triple10 triple8) -> rule2)) -> rule4))]
("tiger" "sees" "cow" "-")
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
((((triple10 triple8) -> (rule2 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The tiger eats the cow.
True
4
proof
[(((((((triple10) -> rule3)) -> rule4)) -> rule1) OR ((((((triple10) -> rule3)) -> rule5)) -> rule1) OR ((((((triple2) -> rule3)) -> rule4)) -> rule1) OR ((((((triple10 triple8) -> rule2)) -> rule4)) -> rule1))]
("tiger" "eats" "cow" "+")
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
((((((triple10 triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The tiger does not eat the cow.
False
4
inv-proof
[(((((((triple10) -> rule3)) -> rule4)) -> rule1) OR ((((((triple10) -> rule3)) -> rule5)) -> rule1) OR ((((((triple2) -> rule3)) -> rule4)) -> rule1) OR ((((((triple10 triple8) -> rule2)) -> rule4)) -> rule1))]
("tiger" "eats" "cow" "-")
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
((((((triple10 triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The squirrel does not see the tiger.
Unknown
inv-random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "-")
The cow sees the tiger.
Unknown
random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow needs the squirrel.[(triple1)] The cow sees the squirrel.[(triple2)] The squirrel eats the cow.[(triple3 OR ((triple6) -> rule1) OR ((((((triple10 triple8) -> rule2)) -> rule5)) -> rule1))] The squirrel is green.[(triple4)] The squirrel needs the tiger.[(triple5)] The squirrel sees the cow.[(triple6 OR ((((triple10 triple8) -> rule2)) -> rule5))] The tiger eats the squirrel.[(triple7)] The tiger is green.[(triple8)] The tiger is round.[(triple9)] The tiger sees the squirrel.[(triple10)] @1: The cow eats the tiger.[(((triple2) -> rule3))] The squirrel eats the tiger.[(((triple10 triple8) -> rule2))] The tiger eats the tiger.[(((triple10) -> rule3))] The tiger is big.[(((triple5) -> rule6))] @2: The cow sees the cow.[(((((triple2) -> rule3)) -> rule5))] The tiger sees the cow.[(((((triple10) -> rule3)) -> rule4) OR ((((triple10) -> rule3)) -> rule5) OR ((((triple2) -> rule3)) -> rule4) OR ((((triple10 triple8) -> rule2)) -> rule4))] @3: The cow eats the cow.[(((((((triple2) -> rule3)) -> rule5)) -> rule1))] The tiger eats the cow.[(((((((triple10) -> rule3)) -> rule4)) -> rule1) OR ((((((triple10) -> rule3)) -> rule5)) -> rule1) OR ((((((triple2) -> rule3)) -> rule4)) -> rule1) OR ((((((triple10 triple8) -> rule2)) -> rule4)) -> rule1))]
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple3
((triple6) -> (rule1 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
((((((triple10 triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
triple4
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple5
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple6
((((triple10 triple8) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple10
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((triple2) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
((triple10 triple8) -> (rule2 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple10) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((triple5) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The tiger sees the cow.
("tiger" "sees" "cow" "+")
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
((((triple10 triple8) -> (rule2 % int2))) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
The tiger eats the cow.
("tiger" "eats" "cow" "+")
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
((((((triple10 triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3