The cat chases the tiger. The cat is big. The cat is blue. The cat is cold. The cat is green. The cat is kind. The cat likes the tiger. The cat needs the tiger. The tiger chases the cat. The tiger is blue. The tiger is cold. The tiger is green. The tiger is kind. The tiger likes the cat. The tiger needs the cat. If someone likes the cat and the cat likes the tiger then they chase the cat. If someone chases the tiger then they need the tiger. If someone chases the cat and they like the cat then they chase the tiger. If someone is blue and they chase the tiger then they like the tiger. Big people are green. If someone is green and they need the tiger then they are cold. If someone needs the cat then the cat is kind. If someone needs the tiger then they chase the tiger.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If someone likes the cat and the cat likes the tiger then they chase the cat.
((("someone" "likes" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the tiger then they need the tiger.
((("someone" "chases" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
If someone chases the cat and they like the cat then they chase the tiger.
((("someone" "chases" "cat" "+") ("someone" "likes" "cat" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is blue and they chase the tiger then they like the tiger.
((("someone" "is" "blue" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "likes" "tiger" "+"))
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is green and they need the tiger then they are cold.
((("someone" "is" "green" "+") ("someone" "needs" "tiger" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the cat then the cat is kind.
((("someone" "needs" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone needs the tiger then they chase the tiger.
((("someone" "needs" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
The tiger likes the cat.
True
1
proof
[(triple14)]
("tiger" "likes" "cat" "+")
triple14
The cat does not need the tiger.
False
1
inv-proof
[(triple8 OR ((triple1) -> rule2))]
("cat" "needs" "tiger" "-")
triple8
((triple1) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger chases the tiger.
True
3
proof
[(((triple9 triple14) -> rule3) OR ((((triple14 triple7) -> rule1) triple14) -> rule3) OR ((((triple14 ((triple3 triple1) -> rule4)) -> rule1) triple14) -> rule3) OR ((((triple14 ((triple3 ((triple8) -> rule8)) -> rule4)) -> rule1) triple14) -> rule3))]
("tiger" "chases" "tiger" "+")
((triple9 triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
((((triple14 triple7) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
((((triple14 ((triple3 triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
((((triple14 ((triple3 ((triple8) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int4
The tiger does not chase the tiger.
False
3
inv-proof
[(((triple9 triple14) -> rule3) OR ((((triple14 triple7) -> rule1) triple14) -> rule3) OR ((((triple14 ((triple3 triple1) -> rule4)) -> rule1) triple14) -> rule3) OR ((((triple14 ((triple3 ((triple8) -> rule8)) -> rule4)) -> rule1) triple14) -> rule3))]
("tiger" "chases" "tiger" "-")
((triple9 triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
((((triple14 triple7) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
((((triple14 ((triple3 triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
((((triple14 ((triple3 ((triple8) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int4
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "cat" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat chases the tiger.[(triple1 OR ((triple8) -> rule8))] The cat is big.[(triple2)] The cat is blue.[(triple3)] The cat is cold.[(triple4 OR ((triple5 triple8) -> rule6) OR ((triple5 ((triple1) -> rule2)) -> rule6) OR ((((triple2) -> rule5) triple8) -> rule6) OR ((((triple2) -> rule5) ((triple1) -> rule2)) -> rule6))] The cat is green.[(triple5 OR ((triple2) -> rule5))] The cat is kind.[(triple6 OR ((triple15) -> rule7))] The cat likes the tiger.[(triple7 OR ((triple3 triple1) -> rule4) OR ((triple3 ((triple8) -> rule8)) -> rule4))] The cat needs the tiger.[(triple8 OR ((triple1) -> rule2))] The tiger chases the cat.[(triple9 OR ((triple14 triple7) -> rule1) OR ((triple14 ((triple3 triple1) -> rule4)) -> rule1) OR ((triple14 ((triple3 ((triple8) -> rule8)) -> rule4)) -> rule1))] The tiger is blue.[(triple10)] The tiger is cold.[(triple11 OR ((triple12 ((((triple9 triple14) -> rule3)) -> rule2)) -> rule6) OR ((triple12 ((((((triple14 triple7) -> rule1) triple14) -> rule3)) -> rule2)) -> rule6) OR ((triple12 ((((((triple14 ((triple3 triple1) -> rule4)) -> rule1) triple14) -> rule3)) -> rule2)) -> rule6) OR ((triple12 ((((((triple14 ((triple3 ((triple8) -> rule8)) -> rule4)) -> rule1) triple14) -> rule3)) -> rule2)) -> rule6))] The tiger is green.[(triple12)] The tiger is kind.[(triple13)] The tiger likes the cat.[(triple14)] The tiger needs the cat.[(triple15)] @1: The tiger chases the tiger.[(((triple9 triple14) -> rule3) OR ((((triple14 triple7) -> rule1) triple14) -> rule3) OR ((((triple14 ((triple3 triple1) -> rule4)) -> rule1) triple14) -> rule3) OR ((((triple14 ((triple3 ((triple8) -> rule8)) -> rule4)) -> rule1) triple14) -> rule3))] @2: The tiger likes the tiger.[(((triple10 ((triple9 triple14) -> rule3)) -> rule4) OR ((triple10 ((((triple14 triple7) -> rule1) triple14) -> rule3)) -> rule4) OR ((triple10 ((((triple14 ((triple3 triple1) -> rule4)) -> rule1) triple14) -> rule3)) -> rule4) OR ((triple10 ((((triple14 ((triple3 ((triple8) -> rule8)) -> rule4)) -> rule1) triple14) -> rule3)) -> rule4))] The tiger needs the tiger.[(((((triple9 triple14) -> rule3)) -> rule2) OR ((((((triple14 triple7) -> rule1) triple14) -> rule3)) -> rule2) OR ((((((triple14 ((triple3 triple1) -> rule4)) -> rule1) triple14) -> rule3)) -> rule2) OR ((((((triple14 ((triple3 ((triple8) -> rule8)) -> rule4)) -> rule1) triple14) -> rule3)) -> rule2))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
((triple8) -> (rule8 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is cold.
("cat" "is" "cold" "+")
triple4
((triple5 triple8) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple5 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple2) -> (rule5 % int2)) triple8) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
((((triple2) -> (rule5 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The cat is green.
("cat" "is" "green" "+")
triple5
((triple2) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
triple6
((triple15) -> (rule7 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple7
((triple3 triple1) -> (rule4 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
((triple3 ((triple8) -> (rule8 % int2))) -> (rule4 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple8
((triple1) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple9
((triple14 triple7) -> (rule1 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
((triple14 ((triple3 triple1) -> (rule4 % int2))) -> (rule1 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
((triple14 ((triple3 ((triple8) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
((triple12 ((((triple9 triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
((triple12 ((((((triple14 triple7) -> (rule1 % int4)) triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
((triple12 ((((((triple14 ((triple3 triple1) -> (rule4 % int5))) -> (rule1 % int4)) triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int5
((triple12 ((((((triple14 ((triple3 ((triple8) -> (rule8 % int6))) -> (rule4 % int5))) -> (rule1 % int4)) triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int5
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int6
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple14
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple9 triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
((((triple14 triple7) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
((((triple14 ((triple3 triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
((((triple14 ((triple3 ((triple8) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int4
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple10 ((triple9 triple14) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
((triple10 ((((triple14 triple7) -> (rule1 % int3)) triple14) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
((triple10 ((((triple14 ((triple3 triple1) -> (rule4 % int4))) -> (rule1 % int3)) triple14) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
((triple10 ((((triple14 ((triple3 ((triple8) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) triple14) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int5
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple9 triple14) -> (rule3 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
((((((triple14 triple7) -> (rule1 % int3)) triple14) -> (rule3 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
((((((triple14 ((triple3 triple1) -> (rule4 % int4))) -> (rule1 % int3)) triple14) -> (rule3 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
((((((triple14 ((triple3 ((triple8) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) triple14) -> (rule3 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int5