The cat eats the rabbit. The dog likes the mouse. The mouse likes the cat. The rabbit eats the mouse. If someone likes the mouse and the mouse is big then they like the dog. If someone is young and rough then they like the rabbit. If someone eats the mouse then the mouse is rough. If someone is rough then they chase the rabbit. If someone is nice then they like the cat. If someone likes the mouse and the mouse is nice then the mouse is rough.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
If someone likes the mouse and the mouse is big then they like the dog.
((("someone" "likes" "mouse" "+") ("mouse" "is" "big" "+")) -> ("someone" "likes" "dog" "+"))
If someone is young and rough then they like the rabbit.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone eats the mouse then the mouse is rough.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If someone is rough then they chase the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone is nice then they like the cat.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "cat" "+"))
If someone likes the mouse and the mouse is nice then the mouse is rough.
((("someone" "likes" "mouse" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "is" "rough" "+"))
The dog likes the mouse.
True
1
proof
[(triple2)]
("dog" "likes" "mouse" "+")
triple2
The dog does not like the mouse.
False
1
inv-proof
[(triple2)]
("dog" "likes" "mouse" "-")
triple2
The mouse is rough.
True
2
proof
[(((triple4) -> rule3))]
("mouse" "is" "rough" "+")
((triple4) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("mouse" "is" "rough" "-")
((triple4) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse chases the rabbit.
True
3
proof
[(((((triple4) -> rule3)) -> rule4))]
("mouse" "chases" "rabbit" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not chase the rabbit.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule4))]
("mouse" "chases" "rabbit" "-")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not like the dog.
Unknown
inv-rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "dog" "-")
The cat likes the rabbit.
Unknown
rconc
[@1: The cat likes the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "rabbit" "+")
The rabbit does not like the cat.
Unknown
inv-rconc
[@1: The rabbit likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "likes" "cat" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The rabbit eats the cat.
Unknown
random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "+")
@0: The cat eats the rabbit.[(triple1)] The dog likes the mouse.[(triple2)] The mouse likes the cat.[(triple3)] The rabbit eats the mouse.[(triple4)] @1: The mouse is rough.[(((triple4) -> rule3))] @2: The mouse chases the rabbit.[(((((triple4) -> rule3)) -> rule4))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple3
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
((triple4) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2