The mouse eats the rabbit. The mouse needs the rabbit. The rabbit eats the mouse. If someone sees the mouse then they eat the rabbit. If someone sees the rabbit and the rabbit sees the mouse then the rabbit eats the mouse. If someone sees the rabbit and the rabbit is rough then they need the rabbit. If someone needs the mouse and they eat the rabbit then the mouse sees the rabbit. If someone eats the rabbit then they eat the mouse. If someone needs the rabbit then the rabbit eats the mouse. If someone is round and they need the rabbit then the rabbit sees the mouse. If someone eats the mouse then they see the mouse.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
If someone sees the mouse then they eat the rabbit.
((("someone" "sees" "mouse" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone sees the rabbit and the rabbit sees the mouse then the rabbit eats the mouse.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "mouse" "+")) -> ("rabbit" "eats" "mouse" "+"))
If someone sees the rabbit and the rabbit is rough then they need the rabbit.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the mouse and they eat the rabbit then the mouse sees the rabbit.
((("someone" "needs" "mouse" "+") ("someone" "eats" "rabbit" "+")) -> ("mouse" "sees" "rabbit" "+"))
If someone eats the rabbit then they eat the mouse.
((("someone" "eats" "rabbit" "+")) -> ("someone" "eats" "mouse" "+"))
If someone needs the rabbit then the rabbit eats the mouse.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "+"))
If someone is round and they need the rabbit then the rabbit sees the mouse.
((("someone" "is" "round" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
If someone eats the mouse then they see the mouse.
((("someone" "eats" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
The mouse eats the rabbit.
True
1
proof
[(triple1)]
("mouse" "eats" "rabbit" "+")
triple1
The mouse does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("mouse" "eats" "rabbit" "-")
triple1
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The mouse eats the rabbit.[(triple1)] The mouse needs the rabbit.[(triple2)] The rabbit eats the mouse.[(triple3 OR ((triple2) -> rule6))] @1: The mouse eats the mouse.[(((triple1) -> rule5))] The rabbit sees the mouse.[(((triple3) -> rule8) OR ((((triple2) -> rule6)) -> rule8))] @2: The mouse sees the mouse.[(((((triple1) -> rule5)) -> rule8))] The rabbit eats the rabbit.[(((((triple3) -> rule8)) -> rule1) OR ((((((triple2) -> rule6)) -> rule8)) -> rule1))]
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple3
((triple2) -> (rule6 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple1) -> (rule5 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((triple3) -> (rule8 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3