The mouse sees the rabbit. The rabbit chases the mouse. The rabbit sees the mouse. If someone sees the mouse then the mouse is round. If someone chases the mouse and they chase the rabbit then they need the mouse. If someone needs the mouse then the mouse sees the rabbit. If someone chases the mouse and they need the rabbit then the mouse sees the rabbit. If someone sees the rabbit and the rabbit chases the mouse then the rabbit needs the mouse. If someone sees the mouse and the mouse needs the rabbit then the rabbit is young. If someone is round then they chase the mouse. If someone needs the mouse then the mouse needs the rabbit.
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone sees the mouse then the mouse is round.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If someone chases the mouse and they chase the rabbit then they need the mouse.
((("someone" "chases" "mouse" "+") ("someone" "chases" "rabbit" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the mouse then the mouse sees the rabbit.
((("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If someone chases the mouse and they need the rabbit then the mouse sees the rabbit.
((("someone" "chases" "mouse" "+") ("someone" "needs" "rabbit" "+")) -> ("mouse" "sees" "rabbit" "+"))
If someone sees the rabbit and the rabbit chases the mouse then the rabbit needs the mouse.
((("someone" "sees" "rabbit" "+") ("rabbit" "chases" "mouse" "+")) -> ("rabbit" "needs" "mouse" "+"))
If someone sees the mouse and the mouse needs the rabbit then the rabbit is young.
((("someone" "sees" "mouse" "+") ("mouse" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone is round then they chase the mouse.
((("someone" "is" "round" "+")) -> ("someone" "chases" "mouse" "+"))
If someone needs the mouse then the mouse needs the rabbit.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple3)]
("rabbit" "sees" "mouse" "+")
triple3
The mouse does not see the rabbit.
False
1
inv-proof
[(triple1)]
("mouse" "sees" "rabbit" "-")
triple1
The mouse is round.
True
2
proof
[(((triple3) -> rule1))]
("mouse" "is" "round" "+")
((triple3) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The rabbit does not need the mouse.
False
3
inv-proof
[(((triple1 triple2) -> rule5))]
("rabbit" "needs" "mouse" "-")
((triple1 triple2) -> (rule5 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The mouse needs the rabbit.
True
4
proof
[(((((triple1 triple2) -> rule5)) -> rule8))]
("mouse" "needs" "rabbit" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule8 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int2
The mouse does not need the rabbit.
False
4
inv-proof
[(((((triple1 triple2) -> rule5)) -> rule8))]
("mouse" "needs" "rabbit" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule8 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int2
The rabbit is young.
True
6
proof
[(((triple3 ((((triple1 triple2) -> rule5)) -> rule8)) -> rule6))]
("rabbit" "is" "young" "+")
((triple3 ((((triple1 triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3
The rabbit is not young.
False
6
inv-proof
[(((triple3 ((((triple1 triple2) -> rule5)) -> rule8)) -> rule6))]
("rabbit" "is" "young" "-")
((triple3 ((((triple1 triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse chases the rabbit.
Unknown
random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The mouse sees the rabbit.[(triple1)] The rabbit chases the mouse.[(triple2)] The rabbit sees the mouse.[(triple3)] @1: The mouse is round.[(((triple3) -> rule1))] The rabbit needs the mouse.[(((triple1 triple2) -> rule5))] @2: The mouse chases the mouse.[(((((triple3) -> rule1)) -> rule7))] The mouse needs the rabbit.[(((((triple1 triple2) -> rule5)) -> rule8))] @3: The rabbit is young.[(((triple3 ((((triple1 triple2) -> rule5)) -> rule8)) -> rule6))]
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
((triple3) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((triple1 triple2) -> (rule5 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule8 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
((triple3 ((((triple1 triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3