The mouse chases the rabbit. The mouse is big. The mouse likes the rabbit. The rabbit is nice. The rabbit is red. The rabbit likes the mouse. The rabbit needs the mouse. If the rabbit likes the mouse then the rabbit is cold. If someone needs the mouse then the mouse needs the rabbit. If someone is green then they chase the rabbit. If someone chases the mouse then they are big. If someone needs the rabbit then the rabbit is green. If someone is nice and they like the rabbit then the rabbit is big.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If the rabbit likes the mouse then the rabbit is cold.
((("rabbit" "likes" "mouse" "+")) -> ("rabbit" "is" "cold" "+"))
If someone needs the mouse then the mouse needs the rabbit.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If someone is green then they chase the rabbit.
((("someone" "is" "green" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the mouse then they are big.
((("someone" "chases" "mouse" "+")) -> ("someone" "is" "big" "+"))
If someone needs the rabbit then the rabbit is green.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If someone is nice and they like the rabbit then the rabbit is big.
((("someone" "is" "nice" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
The mouse chases the rabbit.
True
1
proof
[(triple1)]
("mouse" "chases" "rabbit" "+")
triple1
The rabbit is not nice.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "nice" "-")
triple4
The mouse needs the rabbit.
True
2
proof
[(((triple7) -> rule2))]
("mouse" "needs" "rabbit" "+")
((triple7) -> (rule2 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit is not cold.
False
2
inv-proof
[(((triple6) -> rule1))]
("rabbit" "is" "cold" "-")
((triple6) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is green.
True
3
proof
[(((((triple7) -> rule2)) -> rule5))]
("rabbit" "is" "green" "+")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit is not green.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule5))]
("rabbit" "is" "green" "-")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit chases the rabbit.
True
4
proof
[(((((((triple7) -> rule2)) -> rule5)) -> rule3))]
("rabbit" "chases" "rabbit" "+")
((((((triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3
The rabbit does not chase the rabbit.
False
4
inv-proof
[(((((((triple7) -> rule2)) -> rule5)) -> rule3))]
("rabbit" "chases" "rabbit" "-")
((((((triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "big" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
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 chase the mouse.
Unknown
inv-random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The mouse chases the rabbit.[(triple1)] The mouse is big.[(triple2)] The mouse likes the rabbit.[(triple3)] The rabbit is nice.[(triple4)] The rabbit is red.[(triple5)] The rabbit likes the mouse.[(triple6)] The rabbit needs the mouse.[(triple7)] @1: The mouse needs the rabbit.[(((triple7) -> rule2))] The rabbit is cold.[(((triple6) -> rule1))] @2: The rabbit is green.[(((((triple7) -> rule2)) -> rule5))] @3: The rabbit chases the rabbit.[(((((((triple7) -> rule2)) -> rule5)) -> rule3))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple6
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple7
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((triple7) -> (rule2 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple6) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((((triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3