The cat likes the rabbit. The rabbit is green. If the rabbit sees the cat then the rabbit likes the cat. If someone likes the cat then the cat is not big. If someone is kind and they like the cat then they like the rabbit. If someone eats the rabbit then the rabbit sees the cat. If someone likes the rabbit then the rabbit sees the cat. If someone eats the rabbit and the rabbit eats the cat then the rabbit is nice. If someone eats the cat then the cat likes the rabbit. If someone likes the cat and they like the rabbit then they do not eat the cat.
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
If the rabbit sees the cat then the rabbit likes the cat.
((("rabbit" "sees" "cat" "+")) -> ("rabbit" "likes" "cat" "+"))
If someone likes the cat then the cat is not big.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "big" "-"))
If someone is kind and they like the cat then they like the rabbit.
((("someone" "is" "kind" "+") ("someone" "likes" "cat" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone eats the rabbit then the rabbit sees the cat.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If someone likes the rabbit then the rabbit sees the cat.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If someone eats the rabbit and the rabbit eats the cat then the rabbit is nice.
((("someone" "eats" "rabbit" "+") ("rabbit" "eats" "cat" "+")) -> ("rabbit" "is" "nice" "+"))
If someone eats the cat then the cat likes the rabbit.
((("someone" "eats" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
If someone likes the cat and they like the rabbit then they do not eat the cat.
((("someone" "likes" "cat" "+") ("someone" "likes" "rabbit" "+")) -> ("someone" "eats" "cat" "-"))
The cat likes the rabbit.
True
1
proof
[(triple1)]
("cat" "likes" "rabbit" "+")
triple1
The cat does not like the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "likes" "rabbit" "-")
triple1
The rabbit sees the cat.
True
2
proof
[(((triple1) -> rule5))]
("rabbit" "sees" "cat" "+")
((triple1) -> (rule5 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit does not see the cat.
False
2
inv-proof
[(((triple1) -> rule5))]
("rabbit" "sees" "cat" "-")
((triple1) -> (rule5 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit likes the cat.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("rabbit" "likes" "cat" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit does not like the cat.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("rabbit" "likes" "cat" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat is not big.
True
4
proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule2))]
("cat" "is" "big" "-")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The cat is big.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule2))]
("cat" "is" "big" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The rabbit does not eat the cat.
Unknown
inv-random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat likes the rabbit.[(triple1)] The rabbit is green.[(triple2)] @1: The rabbit sees the cat.[(((triple1) -> rule5))] @2: The rabbit likes the cat.[(((((triple1) -> rule5)) -> rule1))] @3: The cat is not big.[(((((((triple1) -> rule5)) -> rule1)) -> rule2))]
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple1) -> (rule5 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat is not big.
("cat" "is" "big" "-")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3