The cat chases the tiger. The cat eats the tiger. The cat is green. The cat likes the tiger. The tiger chases the cat. The tiger eats the cat. The tiger likes the cat. If the tiger eats the cat then the cat is red. If the cat eats the tiger and the cat is young then the tiger is green. If someone chases the tiger then the tiger likes the cat. If someone is green then they like the tiger. If someone eats the cat and they chase the cat then the cat chases the tiger. If someone likes the cat then the cat chases the tiger. If someone eats the cat and they like the tiger then the cat chases the tiger. If someone likes the tiger then they are young.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is green.
("cat" "is" "green" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If the tiger eats the cat then the cat is red.
((("tiger" "eats" "cat" "+")) -> ("cat" "is" "red" "+"))
If the cat eats the tiger and the cat is young then the tiger is green.
((("cat" "eats" "tiger" "+") ("cat" "is" "young" "+")) -> ("tiger" "is" "green" "+"))
If someone chases the tiger then the tiger likes the cat.
((("someone" "chases" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If someone is green then they like the tiger.
((("someone" "is" "green" "+")) -> ("someone" "likes" "tiger" "+"))
If someone eats the cat and they chase the cat then the cat chases the tiger.
((("someone" "eats" "cat" "+") ("someone" "chases" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If someone likes the cat then the cat chases the tiger.
((("someone" "likes" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If someone eats the cat and they like the tiger then the cat chases the tiger.
((("someone" "eats" "cat" "+") ("someone" "likes" "tiger" "+")) -> ("cat" "chases" "tiger" "+"))
If someone likes the tiger then they are young.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "young" "+"))
The tiger likes the cat.
True
1
proof
[(triple7 OR ((triple1) -> rule3) OR ((((triple6 triple5) -> rule5)) -> rule3) OR ((((triple6 ((((triple2 ((triple4) -> rule8)) -> rule2)) -> rule4)) -> rule7)) -> rule3) OR ((((triple6 ((((triple2 ((((triple3) -> rule4)) -> rule8)) -> rule2)) -> rule4)) -> rule7)) -> rule3))]
("tiger" "likes" "cat" "+")
triple7
((triple1) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
((((triple6 triple5) -> (rule5 % int2))) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
((((triple6 ((((triple2 ((triple4) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4
The cat is young.
("cat" "is" "young" "+")
int5
((((triple6 ((((triple2 ((((triple3) -> (rule4 % int6))) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4
The cat is young.
("cat" "is" "young" "+")
int5
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int6
The cat does not like the tiger.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule4))]
("cat" "likes" "tiger" "-")
triple4
((triple3) -> (rule4 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is young.
True
2
proof
[(((triple4) -> rule8) OR ((((triple3) -> rule4)) -> rule8))]
("cat" "is" "young" "+")
((triple4) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The cat is not young.
False
2
inv-proof
[(((triple4) -> rule8) OR ((((triple3) -> rule4)) -> rule8))]
("cat" "is" "young" "-")
((triple4) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The tiger is green.
True
4
proof
[(((triple2 ((triple4) -> rule8)) -> rule2) OR ((triple2 ((((triple3) -> rule4)) -> rule8)) -> rule2))]
("tiger" "is" "green" "+")
((triple2 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The tiger is not green.
False
4
inv-proof
[(((triple2 ((triple4) -> rule8)) -> rule2) OR ((triple2 ((((triple3) -> rule4)) -> rule8)) -> rule2))]
("tiger" "is" "green" "-")
((triple2 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The cat chases the tiger.[(triple1 OR ((triple7) -> rule6) OR ((triple6 triple5) -> rule5) OR ((triple6 ((((triple2 ((triple4) -> rule8)) -> rule2)) -> rule4)) -> rule7) OR ((triple6 ((((triple2 ((((triple3) -> rule4)) -> rule8)) -> rule2)) -> rule4)) -> rule7))] The cat eats the tiger.[(triple2)] The cat is green.[(triple3)] The cat likes the tiger.[(triple4 OR ((triple3) -> rule4))] The tiger chases the cat.[(triple5)] The tiger eats the cat.[(triple6)] The tiger likes the cat.[(triple7 OR ((triple1) -> rule3) OR ((((triple6 triple5) -> rule5)) -> rule3) OR ((((triple6 ((((triple2 ((triple4) -> rule8)) -> rule2)) -> rule4)) -> rule7)) -> rule3) OR ((((triple6 ((((triple2 ((((triple3) -> rule4)) -> rule8)) -> rule2)) -> rule4)) -> rule7)) -> rule3))] @1: The cat is red.[(((triple6) -> rule1))] The cat is young.[(((triple4) -> rule8) OR ((((triple3) -> rule4)) -> rule8))] @2: The tiger is green.[(((triple2 ((triple4) -> rule8)) -> rule2) OR ((triple2 ((((triple3) -> rule4)) -> rule8)) -> rule2))] @3: The tiger likes the tiger.[(((((triple2 ((triple4) -> rule8)) -> rule2)) -> rule4) OR ((((triple2 ((((triple3) -> rule4)) -> rule8)) -> rule2)) -> rule4))] @4: The tiger is young.[(((((((triple2 ((triple4) -> rule8)) -> rule2)) -> rule4)) -> rule8) OR ((((((triple2 ((((triple3) -> rule4)) -> rule8)) -> rule2)) -> rule4)) -> rule8))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
((triple7) -> (rule6 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
((triple6 triple5) -> (rule5 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
((triple6 ((((triple2 ((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
((triple6 ((((triple2 ((((triple3) -> (rule4 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int5
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple4
((triple3) -> (rule4 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple5
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple6
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple7
((triple1) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
((((triple6 triple5) -> (rule5 % int2))) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
((((triple6 ((((triple2 ((triple4) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4
The cat is young.
("cat" "is" "young" "+")
int5
((((triple6 ((((triple2 ((((triple3) -> (rule4 % int6))) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4
The cat is young.
("cat" "is" "young" "+")
int5
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int6
The cat is red.
("cat" "is" "red" "+")
((triple6) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((triple4) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((triple2 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple2 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
((((triple2 ((((triple3) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
The tiger is young.
("tiger" "is" "young" "+")
((((((triple2 ((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
((((((triple2 ((((triple3) -> (rule4 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int5