The cat eats the tiger. The cat sees the tiger. The tiger eats the cat. If someone eats the cat then they like the tiger. If someone likes the tiger then they see the tiger. If someone likes the tiger and the tiger is rough then the tiger likes the cat. If someone eats the cat then the cat is round. If someone eats the tiger and they like the tiger then the tiger is big. If someone is green then they see the tiger. If someone likes the tiger and they see the tiger then the tiger sees the cat. If the tiger sees the cat and the tiger eats the cat then the tiger is round.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
If someone eats the cat then they like the tiger.
((("someone" "eats" "cat" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the tiger then they see the tiger.
((("someone" "likes" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
If someone likes the tiger and the tiger is rough then the tiger likes the cat.
((("someone" "likes" "tiger" "+") ("tiger" "is" "rough" "+")) -> ("tiger" "likes" "cat" "+"))
If someone eats the cat then the cat is round.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "round" "+"))
If someone eats the tiger and they like the tiger then the tiger is big.
((("someone" "eats" "tiger" "+") ("someone" "likes" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If someone is green then they see the tiger.
((("someone" "is" "green" "+")) -> ("someone" "sees" "tiger" "+"))
If someone likes the tiger and they see the tiger then the tiger sees the cat.
((("someone" "likes" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "cat" "+"))
If the tiger sees the cat and the tiger eats the cat then the tiger is round.
((("tiger" "sees" "cat" "+") ("tiger" "eats" "cat" "+")) -> ("tiger" "is" "round" "+"))
The cat eats the tiger.
True
1
proof
[(triple1)]
("cat" "eats" "tiger" "+")
triple1
The tiger does not eat the cat.
False
1
inv-proof
[(triple3)]
("tiger" "eats" "cat" "-")
triple3
The tiger likes the tiger.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "likes" "tiger" "+")
((triple3) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The cat is not round.
False
2
inv-proof
[(((triple3) -> rule4))]
("cat" "is" "round" "-")
((triple3) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger sees the tiger.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("tiger" "sees" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("tiger" "sees" "tiger" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger sees the cat.
True
6
proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule2)) -> rule7))]
("tiger" "sees" "cat" "+")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger does not see the cat.
False
6
inv-proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule2)) -> rule7))]
("tiger" "sees" "cat" "-")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The cat does not like the tiger.
Unknown
inv-rconc
[@1: The cat likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "tiger" "-")
The tiger likes the cat.
Unknown
rconc
[@1: The tiger likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "cat" "+")
The tiger is not big.
Unknown
inv-rconc
[@2: The tiger is big.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("tiger" "is" "big" "-")
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 rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
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 is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat eats the tiger.[(triple1)] The cat sees the tiger.[(triple2)] The tiger eats the cat.[(triple3)] @1: The cat is round.[(((triple3) -> rule4))] The tiger likes the tiger.[(((triple3) -> rule1))] @2: The tiger sees the tiger.[(((((triple3) -> rule1)) -> rule2))] @3: The tiger sees the cat.[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule2)) -> rule7))] @4: The tiger is round.[(((((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule2)) -> rule7) triple3) -> rule8))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
((triple3) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple3) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
((((((triple3) -> (rule1 % int4)) ((((triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule8 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4