The cat sees the dog. The cat sees the tiger. The dog eats the cat. The dog likes the tiger. The rabbit is big. The tiger likes the cat. The tiger sees the cat. If something is green then it likes the tiger. If something sees the rabbit then it is green. If the rabbit is cold and the rabbit is green then the rabbit likes the tiger. If something eats the tiger then the tiger sees the rabbit. If something eats the cat and the cat eats the rabbit then it sees the tiger. If something is cold then it eats the cat. If something likes the cat then the cat eats the dog. If something is big then it eats the tiger.
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something is green then it likes the tiger.
((("something" "is" "green" "+")) -> ("something" "likes" "tiger" "+"))
If something sees the rabbit then it is green.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "green" "+"))
If the rabbit is cold and the rabbit is green then the rabbit likes the tiger.
((("rabbit" "is" "cold" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "likes" "tiger" "+"))
If something eats the tiger then the tiger sees the rabbit.
((("something" "eats" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If something eats the cat and the cat eats the rabbit then it sees the tiger.
((("something" "eats" "cat" "+") ("cat" "eats" "rabbit" "+")) -> ("something" "sees" "tiger" "+"))
If something is cold then it eats the cat.
((("something" "is" "cold" "+")) -> ("something" "eats" "cat" "+"))
If something likes the cat then the cat eats the dog.
((("something" "likes" "cat" "+")) -> ("cat" "eats" "dog" "+"))
If something is big then it eats the tiger.
((("something" "is" "big" "+")) -> ("something" "eats" "tiger" "+"))
The cat sees the tiger.
True
1
proof
[(triple2)]
("cat" "sees" "tiger" "+")
triple2
The tiger does not see the cat.
False
1
inv-proof
[(triple7)]
("tiger" "sees" "cat" "-")
triple7
The cat eats the dog.
True
2
proof
[(((triple6) -> rule7))]
("cat" "eats" "dog" "+")
((triple6) -> (rule7 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cat does not eat the dog.
False
2
inv-proof
[(((triple6) -> rule7))]
("cat" "eats" "dog" "-")
((triple6) -> (rule7 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The tiger sees the rabbit.
True
3
proof
[(((((triple5) -> rule8)) -> rule4))]
("tiger" "sees" "rabbit" "+")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The tiger does not see the rabbit.
False
3
inv-proof
[(((((triple5) -> rule8)) -> rule4))]
("tiger" "sees" "rabbit" "-")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The tiger is green.
True
4
proof
[(((((((triple5) -> rule8)) -> rule4)) -> rule2))]
("tiger" "is" "green" "+")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The tiger is not green.
False
4
inv-proof
[(((((((triple5) -> rule8)) -> rule4)) -> rule2))]
("tiger" "is" "green" "-")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "green" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The rabbit does not eat the cat.
Unknown
inv-rconc
[@1: The rabbit eats the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "cat" "-")
The rabbit sees the tiger.
Unknown
rconc
[@1: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "sees" "tiger" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The tiger eats the rabbit.
Unknown
random
[@0: The tiger eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "rabbit" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The cat sees the dog.[(triple1)] The cat sees the tiger.[(triple2)] The dog eats the cat.[(triple3)] The dog likes the tiger.[(triple4)] The rabbit is big.[(triple5)] The tiger likes the cat.[(triple6)] The tiger sees the cat.[(triple7)] @1: The cat eats the dog.[(((triple6) -> rule7))] The rabbit eats the tiger.[(((triple5) -> rule8))] @2: The tiger sees the rabbit.[(((((triple5) -> rule8)) -> rule4))] @3: The tiger is green.[(((((((triple5) -> rule8)) -> rule4)) -> rule2))] @4: The tiger likes the tiger.[(((((((((triple5) -> rule8)) -> rule4)) -> rule2)) -> rule1))]
The cat sees the dog.
("cat" "sees" "dog" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The dog eats the cat.
("dog" "eats" "cat" "+")
triple3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
triple5
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple6
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple7
The cat eats the dog.
("cat" "eats" "dog" "+")
((triple6) -> (rule7 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
((triple5) -> (rule8 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((((triple5) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int4