The cat likes the tiger. The cat visits the tiger. The tiger is big. The tiger is red. The tiger likes the cat. The tiger needs the cat. The tiger visits the cat. If something likes the tiger and it visits the cat then it visits the tiger. If something needs the tiger then it likes the cat. If the tiger is big then the tiger needs the cat. If the tiger visits the cat then the cat likes the tiger. If something is kind then it visits the cat. If the tiger needs the cat then the cat needs the tiger. If something likes the tiger then the tiger likes the cat. If something likes the cat then it is rough.
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something likes the tiger and it visits the cat then it visits the tiger.
((("something" "likes" "tiger" "+") ("something" "visits" "cat" "+")) -> ("something" "visits" "tiger" "+"))
If something needs the tiger then it likes the cat.
((("something" "needs" "tiger" "+")) -> ("something" "likes" "cat" "+"))
If the tiger is big then the tiger needs the cat.
((("tiger" "is" "big" "+")) -> ("tiger" "needs" "cat" "+"))
If the tiger visits the cat then the cat likes the tiger.
((("tiger" "visits" "cat" "+")) -> ("cat" "likes" "tiger" "+"))
If something is kind then it visits the cat.
((("something" "is" "kind" "+")) -> ("something" "visits" "cat" "+"))
If the tiger needs the cat then the cat needs the tiger.
((("tiger" "needs" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If something likes the tiger then the tiger likes the cat.
((("something" "likes" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If something likes the cat then it is rough.
((("something" "likes" "cat" "+")) -> ("something" "is" "rough" "+"))
The tiger needs the cat.
True
1
proof
[(triple6 OR ((triple3) -> rule3))]
("tiger" "needs" "cat" "+")
triple6
((triple3) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger is not big.
False
1
inv-proof
[(triple3)]
("tiger" "is" "big" "-")
triple3
The cat needs the tiger.
True
2
proof
[(((triple6) -> rule6) OR ((((triple3) -> rule3)) -> rule6))]
("cat" "needs" "tiger" "+")
((triple6) -> (rule6 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger is not rough.
False
2
inv-proof
[(((triple5) -> rule8) OR ((((triple1) -> rule7)) -> rule8) OR ((((((triple7) -> rule4)) -> rule7)) -> rule8))]
("tiger" "is" "rough" "-")
((triple5) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
((((((triple7) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat likes the cat.
True
3
proof
[(((((triple6) -> rule6)) -> rule2) OR ((((((triple3) -> rule3)) -> rule6)) -> rule2))]
("cat" "likes" "cat" "+")
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The cat does not like the cat.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule2) OR ((((((triple3) -> rule3)) -> rule6)) -> rule2))]
("cat" "likes" "cat" "-")
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The cat is rough.
True
4
proof
[(((((((triple6) -> rule6)) -> rule2)) -> rule8) OR ((((((((triple3) -> rule3)) -> rule6)) -> rule2)) -> rule8))]
("cat" "is" "rough" "+")
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4
The cat is not rough.
False
4
inv-proof
[(((((((triple6) -> rule6)) -> rule2)) -> rule8) OR ((((((((triple3) -> rule3)) -> rule6)) -> rule2)) -> rule8))]
("cat" "is" "rough" "-")
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "cat" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
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 red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat likes the tiger.[(triple1 OR ((triple7) -> rule4))] The cat visits the tiger.[(triple2)] The tiger is big.[(triple3)] The tiger is red.[(triple4)] The tiger likes the cat.[(triple5 OR ((triple1) -> rule7) OR ((((triple7) -> rule4)) -> rule7))] The tiger needs the cat.[(triple6 OR ((triple3) -> rule3))] The tiger visits the cat.[(triple7)] @1: The cat needs the tiger.[(((triple6) -> rule6) OR ((((triple3) -> rule3)) -> rule6))] The tiger is rough.[(((triple5) -> rule8) OR ((((triple1) -> rule7)) -> rule8) OR ((((((triple7) -> rule4)) -> rule7)) -> rule8))] @2: The cat likes the cat.[(((((triple6) -> rule6)) -> rule2) OR ((((((triple3) -> rule3)) -> rule6)) -> rule2))] @3: The cat is rough.[(((((((triple6) -> rule6)) -> rule2)) -> rule8) OR ((((((((triple3) -> rule3)) -> rule6)) -> rule2)) -> rule8))]
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple1
((triple7) -> (rule4 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple2
The tiger is big.
("tiger" "is" "big" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple5
((triple1) -> (rule7 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule7 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple6
((triple3) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple7
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple6) -> (rule6 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
((triple5) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
((((((triple7) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat likes the cat.
("cat" "likes" "cat" "+")
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4