The mouse is kind. The mouse is young. The rabbit likes the mouse. If something is young then it needs the mouse. If the rabbit likes the mouse and the rabbit needs the mouse then the mouse is young. If something needs the mouse then the mouse does not eat the rabbit. If something likes the rabbit then the rabbit likes the mouse. If something likes the mouse and it is not rough then it eats the rabbit. If the rabbit is rough and the rabbit needs the mouse then the rabbit eats the mouse. If the mouse is nice then the mouse likes the rabbit. If the rabbit needs the mouse and the rabbit does not eat the mouse then the rabbit is nice.
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If something is young then it needs the mouse.
((("something" "is" "young" "+")) -> ("something" "needs" "mouse" "+"))
If the rabbit likes the mouse and the rabbit needs the mouse then the mouse is young.
((("rabbit" "likes" "mouse" "+") ("rabbit" "needs" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If something needs the mouse then the mouse does not eat the rabbit.
((("something" "needs" "mouse" "+")) -> ("mouse" "eats" "rabbit" "-"))
If something likes the rabbit then the rabbit likes the mouse.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If something likes the mouse and it is not rough then it eats the rabbit.
((("something" "likes" "mouse" "+") ("something" "is" "rough" "~")) -> ("something" "eats" "rabbit" "+"))
If the rabbit is rough and the rabbit needs the mouse then the rabbit eats the mouse.
((("rabbit" "is" "rough" "+") ("rabbit" "needs" "mouse" "+")) -> ("rabbit" "eats" "mouse" "+"))
If the mouse is nice then the mouse likes the rabbit.
((("mouse" "is" "nice" "+")) -> ("mouse" "likes" "rabbit" "+"))
If the rabbit needs the mouse and the rabbit does not eat the mouse then the rabbit is nice.
((("rabbit" "needs" "mouse" "+") ("rabbit" "eats" "mouse" "~")) -> ("rabbit" "is" "nice" "+"))
The mouse is kind.
True
1
proof
[(triple1)]
("mouse" "is" "kind" "+")
triple1
The mouse is not young.
False
1
inv-proof
[(triple2)]
("mouse" "is" "young" "-")
triple2
The mouse needs the mouse.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "needs" "mouse" "+")
((triple2) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse does not need the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "needs" "mouse" "-")
((triple2) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse does not eat the rabbit.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("mouse" "eats" "rabbit" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The mouse does not eat the rabbit.
("mouse" "eats" "rabbit" "-")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse eats the rabbit.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("mouse" "eats" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The mouse does not eat the rabbit.
("mouse" "eats" "rabbit" "-")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse does not like the rabbit.
Unknown
inv-rconc
[@1: The mouse likes the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "likes" "rabbit" "-")
The rabbit eats the mouse.
Unknown
rconc
[@1: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "mouse" "+")
The rabbit does not need the mouse.
Unknown
inv-rconc
[@1: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The mouse is kind.[(triple1)] The mouse is young.[(triple2)] The rabbit likes the mouse.[(triple3)] @1: The mouse needs the mouse.[(((triple2) -> rule1))] @2: The mouse does not eat the rabbit.[(((((triple2) -> rule1)) -> rule3))]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1
The mouse is young.
("mouse" "is" "young" "+")
triple2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple3
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple2) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse does not eat the rabbit.
("mouse" "eats" "rabbit" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The mouse does not eat the rabbit.
("mouse" "eats" "rabbit" "-")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2