The cat likes the rabbit. The mouse needs the rabbit. The rabbit likes the mouse. If someone is kind then they like the mouse. If someone needs the rabbit then the rabbit is big. If someone likes the rabbit and the rabbit is big then the rabbit likes the cat.
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If someone is kind then they like the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "mouse" "+"))
If someone needs the rabbit then the rabbit is big.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If someone likes the rabbit and the rabbit is big then the rabbit likes the cat.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("rabbit" "likes" "cat" "+"))
The cat likes the rabbit.
True
1
proof
[(triple1)]
("cat" "likes" "rabbit" "+")
triple1
The mouse does not need the rabbit.
False
1
inv-proof
[(triple2)]
("mouse" "needs" "rabbit" "-")
triple2
The rabbit is big.
True
2
proof
[(((triple2) -> rule2))]
("rabbit" "is" "big" "+")
((triple2) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("rabbit" "is" "big" "-")
((triple2) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit likes the cat.
True
4
proof
[(((triple1 ((triple2) -> rule2)) -> rule3))]
("rabbit" "likes" "cat" "+")
((triple1 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not like the cat.
False
4
inv-proof
[(((triple1 ((triple2) -> rule2)) -> rule3))]
("rabbit" "likes" "cat" "-")
((triple1 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The cat likes the mouse.
Unknown
rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "mouse" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cat likes the rabbit.[(triple1)] The mouse needs the rabbit.[(triple2)] The rabbit likes the mouse.[(triple3)] @1: The rabbit is big.[(((triple2) -> rule2))] @2: The rabbit likes the cat.[(((triple1 ((triple2) -> rule2)) -> rule3))]
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
((triple2) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((triple1 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2