The cat eats the tiger. The cat is green. The cat is rough. The cat is young. The cat likes the tiger. The tiger eats the cat. The tiger is green. The tiger is kind. The tiger is young. The tiger likes the cat. If someone likes the cat and the cat eats the tiger then the cat likes the tiger. If the cat needs the tiger then the cat likes the tiger. If someone eats the tiger then they are rough. If someone is kind then they eat the tiger. If the cat eats the tiger then the tiger needs the cat. If someone likes the tiger and they eat the cat then they need the tiger. If someone is rough then they like the cat. If someone needs the cat then they like the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If someone likes the cat and the cat eats the tiger then the cat likes the tiger.
((("someone" "likes" "cat" "+") ("cat" "eats" "tiger" "+")) -> ("cat" "likes" "tiger" "+"))
If the cat needs the tiger then the cat likes the tiger.
((("cat" "needs" "tiger" "+")) -> ("cat" "likes" "tiger" "+"))
If someone eats the tiger then they are rough.
((("someone" "eats" "tiger" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they eat the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "tiger" "+"))
If the cat eats the tiger then the tiger needs the cat.
((("cat" "eats" "tiger" "+")) -> ("tiger" "needs" "cat" "+"))
If someone likes the tiger and they eat the cat then they need the tiger.
((("someone" "likes" "tiger" "+") ("someone" "eats" "cat" "+")) -> ("someone" "needs" "tiger" "+"))
If someone is rough then they like the cat.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "cat" "+"))
If someone needs the cat then they like the tiger.
((("someone" "needs" "cat" "+")) -> ("someone" "likes" "tiger" "+"))
The tiger is young.
True
1
proof
[(triple9)]
("tiger" "is" "young" "+")
triple9
The tiger does not like the cat.
False
1
inv-proof
[(triple10 OR ((((((triple8) -> rule4)) -> rule3)) -> rule7))]
("tiger" "likes" "cat" "-")
triple10
((((((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The cat likes the cat.
True
2
proof
[(((triple3) -> rule7) OR ((((triple1) -> rule3)) -> rule7))]
("cat" "likes" "cat" "+")
((triple3) -> (rule7 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple8) -> rule4))]
("tiger" "eats" "tiger" "-")
((triple8) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger likes the tiger.
True
3
proof
[(((((triple1) -> rule5)) -> rule8))]
("tiger" "likes" "tiger" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger is not rough.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule3))]
("tiger" "is" "rough" "-")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger needs the tiger.
True
5
proof
[(((((((triple1) -> rule5)) -> rule8) triple6) -> rule6))]
("tiger" "needs" "tiger" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The tiger does not need the tiger.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule8) triple6) -> rule6))]
("tiger" "needs" "tiger" "-")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The cat does not need the tiger.
Unknown
inv-rconc
[@1: The cat needs the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "tiger" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat eats the tiger.[(triple1)] The cat is green.[(triple2)] The cat is rough.[(triple3 OR ((triple1) -> rule3))] The cat is young.[(triple4)] The cat likes the tiger.[(triple5 OR ((triple10 triple1) -> rule1) OR ((((triple3) -> rule7) triple1) -> rule1) OR ((((((triple1) -> rule3)) -> rule7) triple1) -> rule1) OR ((((((((triple8) -> rule4)) -> rule3)) -> rule7) triple1) -> rule1))] The tiger eats the cat.[(triple6)] The tiger is green.[(triple7)] The tiger is kind.[(triple8)] The tiger is young.[(triple9)] The tiger likes the cat.[(triple10 OR ((((((triple8) -> rule4)) -> rule3)) -> rule7))] @1: The cat likes the cat.[(((triple3) -> rule7) OR ((((triple1) -> rule3)) -> rule7))] The tiger eats the tiger.[(((triple8) -> rule4))] The tiger needs the cat.[(((triple1) -> rule5))] @2: The tiger is rough.[(((((triple8) -> rule4)) -> rule3))] The tiger likes the tiger.[(((((triple1) -> rule5)) -> rule8))] @3: The tiger needs the tiger.[(((((((triple1) -> rule5)) -> rule8) triple6) -> rule6))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
((triple1) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
triple4
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple5
((triple10 triple1) -> (rule1 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
((((triple3) -> (rule7 % int2)) triple1) -> (rule1 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2)) triple1) -> (rule1 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((((((triple8) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) triple1) -> (rule1 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int4
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger is kind.
("tiger" "is" "kind" "+")
triple8
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple10
((((((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple3) -> (rule7 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple8) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((triple1) -> (rule5 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3