The mouse chases the rabbit. The mouse is nice. The mouse likes the rabbit. The mouse does not see the rabbit. The rabbit is rough. The rabbit is young. The rabbit likes the mouse. If the mouse sees the rabbit then the rabbit likes the mouse. If the rabbit sees the mouse and the mouse sees the rabbit then the mouse is big. If someone sees the mouse then they like the rabbit. If someone is nice and they like the rabbit then the rabbit is rough. If someone likes the mouse then they see the mouse. If someone likes the rabbit then they chase the rabbit.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If the mouse sees the rabbit then the rabbit likes the mouse.
((("mouse" "sees" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If the rabbit sees the mouse and the mouse sees the rabbit then the mouse is big.
((("rabbit" "sees" "mouse" "+") ("mouse" "sees" "rabbit" "+")) -> ("mouse" "is" "big" "+"))
If someone sees the mouse then they like the rabbit.
((("someone" "sees" "mouse" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone is nice and they like the rabbit then the rabbit is rough.
((("someone" "is" "nice" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If someone likes the mouse then they see the mouse.
((("someone" "likes" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If someone likes the rabbit then they chase the rabbit.
((("someone" "likes" "rabbit" "+")) -> ("someone" "chases" "rabbit" "+"))
The rabbit is young.
True
1
proof
[(triple6)]
("rabbit" "is" "young" "+")
triple6
The rabbit is not young.
False
1
inv-proof
[(triple6)]
("rabbit" "is" "young" "-")
triple6
The rabbit sees the mouse.
True
2
proof
[(((triple7) -> rule5))]
("rabbit" "sees" "mouse" "+")
((triple7) -> (rule5 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit does not see the mouse.
False
2
inv-proof
[(((triple7) -> rule5))]
("rabbit" "sees" "mouse" "-")
((triple7) -> (rule5 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit likes the rabbit.
True
3
proof
[(((((triple7) -> rule5)) -> rule3))]
("rabbit" "likes" "rabbit" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit does not like the rabbit.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule3))]
("rabbit" "likes" "rabbit" "-")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit chases the rabbit.
True
4
proof
[(((((((triple7) -> rule5)) -> rule3)) -> rule6))]
("rabbit" "chases" "rabbit" "+")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int3
The rabbit does not chase the rabbit.
False
4
inv-proof
[(((((((triple7) -> rule5)) -> rule3)) -> rule6))]
("rabbit" "chases" "rabbit" "-")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int3
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The mouse chases the rabbit.[(triple1 OR ((triple3) -> rule6))] The mouse does not see the rabbit.[(triple4)] The mouse is nice.[(triple2)] The mouse likes the rabbit.[(triple3)] The rabbit is rough.[(triple5 OR ((triple2 triple3) -> rule4))] The rabbit is young.[(triple6)] The rabbit likes the mouse.[(triple7)] @1: The rabbit sees the mouse.[(((triple7) -> rule5))] @2: The rabbit likes the rabbit.[(((((triple7) -> rule5)) -> rule3))] @3: The rabbit chases the rabbit.[(((((((triple7) -> rule5)) -> rule3)) -> rule6))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
((triple3) -> (rule6 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
triple4
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple3
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
((triple2 triple3) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple7
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((triple7) -> (rule5 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int3