The mouse chases the rabbit. The mouse is rough. The rabbit sees the mouse. If the rabbit sees the mouse and the mouse is blue then the rabbit chases the mouse. If someone chases the rabbit then the rabbit eats the mouse.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If the rabbit sees the mouse and the mouse is blue then the rabbit chases the mouse.
((("rabbit" "sees" "mouse" "+") ("mouse" "is" "blue" "+")) -> ("rabbit" "chases" "mouse" "+"))
If someone chases the rabbit then the rabbit eats the mouse.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "+"))
The mouse is rough.
True
1
proof
[(triple2)]
("mouse" "is" "rough" "+")
triple2
The mouse does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("mouse" "chases" "rabbit" "-")
triple1
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The mouse chases the rabbit.[(triple1)] The mouse is rough.[(triple2)] The rabbit sees the mouse.[(triple3)] @1: The rabbit eats the mouse.[(((triple1) -> rule2))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple3
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((triple1) -> (rule2 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1