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