The mouse does not see the rabbit. The rabbit chases the squirrel. The squirrel does not like the mouse. If someone chases the squirrel then they chase the mouse. If someone is nice then they chase the mouse. If the mouse is not red then the mouse sees the squirrel. If someone chases the mouse and they are blue then they are rough. If someone chases the mouse and they chase the squirrel then they do not see the rabbit. If someone chases the rabbit then they do not like the squirrel.
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
If someone chases the squirrel then they chase the mouse.
((("someone" "chases" "squirrel" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is nice then they chase the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "mouse" "+"))
If the mouse is not red then the mouse sees the squirrel.
((("mouse" "is" "red" "~")) -> ("mouse" "sees" "squirrel" "+"))
If someone chases the mouse and they are blue then they are rough.
((("someone" "chases" "mouse" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone chases the mouse and they chase the squirrel then they do not see the rabbit.
((("someone" "chases" "mouse" "+") ("someone" "chases" "squirrel" "+")) -> ("someone" "sees" "rabbit" "-"))
If someone chases the rabbit then they do not like the squirrel.
((("someone" "chases" "rabbit" "+")) -> ("someone" "likes" "squirrel" "-"))
The rabbit chases the squirrel.
True
1
proof
[(triple2)]
("rabbit" "chases" "squirrel" "+")
triple2
The mouse sees the rabbit.
False
1
inv-proof
[(triple1)]
("mouse" "sees" "rabbit" "+")
triple1
The rabbit chases the mouse.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "chases" "mouse" "+")
((triple2) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit does not chase the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "chases" "mouse" "-")
((triple2) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit does not see the rabbit.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule5))]
("rabbit" "sees" "rabbit" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit sees the rabbit.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule5))]
("rabbit" "sees" "rabbit" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The rabbit is rough.
Unknown
rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "rough" "+")
The squirrel does not chase the mouse.
Unknown
inv-rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "mouse" "-")
The rabbit likes the squirrel.
Unknown
random
[@0: The rabbit likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "squirrel" "+")
The squirrel does not chase the rabbit.
Unknown
inv-random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The mouse does not see the rabbit.[(triple1)] The rabbit chases the squirrel.[(triple2)] The squirrel does not like the mouse.[(triple3)] @1: The rabbit chases the mouse.[(((triple2) -> rule1))] @2: The rabbit does not see the rabbit.[(((((triple2) -> rule1) triple2) -> rule5))]
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
triple1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple2
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
triple3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((triple2) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2