The mouse chases the rabbit. The mouse is red. The mouse is round. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit chases the mouse. The rabbit is nice. The rabbit is red. The rabbit needs the mouse. The rabbit sees the mouse. If someone needs the mouse and the mouse chases the rabbit then they chase the rabbit.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone needs the mouse and the mouse chases the rabbit then they chase the rabbit.
((("someone" "needs" "mouse" "+") ("mouse" "chases" "rabbit" "+")) -> ("someone" "chases" "rabbit" "+"))
The rabbit needs the mouse.
True
1
proof
[(triple9)]
("rabbit" "needs" "mouse" "+")
triple9
The mouse is not round.
False
1
inv-proof
[(triple3)]
("mouse" "is" "round" "-")
triple3
The rabbit chases the rabbit.
True
3
proof
[(((triple9 triple1) -> rule1))]
("rabbit" "chases" "rabbit" "+")
((triple9 triple1) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((triple9 triple1) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((triple9 triple1) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The mouse chases the rabbit.[(triple1)] The mouse is red.[(triple2)] The mouse is round.[(triple3)] The mouse needs the rabbit.[(triple4)] The mouse sees the rabbit.[(triple5)] The rabbit chases the mouse.[(triple6)] The rabbit is nice.[(triple7)] The rabbit is red.[(triple8)] The rabbit needs the mouse.[(triple9)] The rabbit sees the mouse.[(triple10)] @1: The rabbit chases the rabbit.[(((triple9 triple1) -> rule1))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse is round.
("mouse" "is" "round" "+")
triple3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple4
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple5
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple9
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple10
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple9 triple1) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1