The mouse visits the rabbit. The rabbit chases the mouse. If the rabbit needs the mouse and the mouse chases the rabbit then the rabbit chases the mouse. If someone is green then they chase the rabbit. If someone chases the mouse then they are green.
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
If the rabbit needs the mouse and the mouse chases the rabbit then the rabbit chases the mouse.
((("rabbit" "needs" "mouse" "+") ("mouse" "chases" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If someone is green then they chase the rabbit.
((("someone" "is" "green" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the mouse then they are green.
((("someone" "chases" "mouse" "+")) -> ("someone" "is" "green" "+"))
The mouse visits the rabbit.
True
1
proof
[(triple1)]
("mouse" "visits" "rabbit" "+")
triple1
The rabbit does not chase the mouse.
False
1
inv-proof
[(triple2)]
("rabbit" "chases" "mouse" "-")
triple2
The rabbit is green.
True
2
proof
[(((triple2) -> rule3))]
("rabbit" "is" "green" "+")
((triple2) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("rabbit" "is" "green" "-")
((triple2) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the rabbit.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("rabbit" "chases" "rabbit" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("rabbit" "chases" "rabbit" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The mouse is not green.
Unknown
inv-rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "green" "-")
The mouse chases the rabbit.
Unknown
rconc
[@2: The mouse chases the rabbit.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("mouse" "chases" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The mouse visits the rabbit.[(triple1)] The rabbit chases the mouse.[(triple2)] @1: The rabbit is green.[(((triple2) -> rule3))] @2: The rabbit chases the rabbit.[(((((triple2) -> rule3)) -> rule2))]
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
((triple2) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2