The mouse chases the rabbit. The mouse is cold. The mouse is rough. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit chases the mouse. The rabbit is big. The rabbit is blue. The rabbit needs the mouse. The rabbit does not see the mouse. If someone needs the rabbit and they do not chase the mouse then the rabbit does not need the mouse. If someone needs the rabbit and they chase the mouse then the mouse is blue. If the mouse is big and the mouse is cold then the mouse is nice. If someone needs the mouse then the mouse chases the rabbit. If someone needs the rabbit then the rabbit is cold. If the mouse needs the rabbit and the rabbit is cold then the mouse is big. If someone is blue and they see the mouse then they need the mouse. If someone sees the mouse then they need the rabbit.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
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 big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
If someone needs the rabbit and they do not chase the mouse then the rabbit does not need the mouse.
((("someone" "needs" "rabbit" "+") ("someone" "chases" "mouse" "~")) -> ("rabbit" "needs" "mouse" "-"))
If someone needs the rabbit and they chase the mouse then the mouse is blue.
((("someone" "needs" "rabbit" "+") ("someone" "chases" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If the mouse is big and the mouse is cold then the mouse is nice.
((("mouse" "is" "big" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "is" "nice" "+"))
If someone needs the mouse then the mouse chases the rabbit.
((("someone" "needs" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
If someone needs the rabbit then the rabbit is cold.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If the mouse needs the rabbit and the rabbit is cold then the mouse is big.
((("mouse" "needs" "rabbit" "+") ("rabbit" "is" "cold" "+")) -> ("mouse" "is" "big" "+"))
If someone is blue and they see the mouse then they need the mouse.
((("someone" "is" "blue" "+") ("someone" "sees" "mouse" "+")) -> ("someone" "needs" "mouse" "+"))
If someone sees the mouse then they need the rabbit.
((("someone" "sees" "mouse" "+")) -> ("someone" "needs" "rabbit" "+"))
The mouse chases the rabbit.
True
1
proof
[(triple1 OR ((triple9) -> rule4))]
("mouse" "chases" "rabbit" "+")
triple1
((triple9) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The rabbit sees the mouse.
False
1
inv-proof
[(triple10)]
("rabbit" "sees" "mouse" "+")
triple10
The rabbit is cold.
True
2
proof
[(((triple4) -> rule5))]
("rabbit" "is" "cold" "+")
((triple4) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is not cold.
False
2
inv-proof
[(((triple4) -> rule5))]
("rabbit" "is" "cold" "-")
((triple4) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse is big.
True
4
proof
[(((triple4 ((triple4) -> rule5)) -> rule6))]
("mouse" "is" "big" "+")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The mouse is not big.
False
4
inv-proof
[(((triple4 ((triple4) -> rule5)) -> rule6))]
("mouse" "is" "big" "-")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The mouse is nice.
True
6
proof
[(((((triple4 ((triple4) -> rule5)) -> rule6) triple2) -> rule3))]
("mouse" "is" "nice" "+")
((((triple4 ((triple4) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The mouse is not nice.
False
6
inv-proof
[(((((triple4 ((triple4) -> rule5)) -> rule6) triple2) -> rule3))]
("mouse" "is" "nice" "-")
((((triple4 ((triple4) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The mouse is not blue.
Unknown
inv-rconc
[@2: The mouse is blue.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("mouse" "is" "blue" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The mouse chases the rabbit.[(triple1 OR ((triple9) -> rule4))] The mouse is cold.[(triple2)] The mouse is rough.[(triple3)] The mouse needs the rabbit.[(triple4)] The mouse sees the rabbit.[(triple5)] The rabbit chases the mouse.[(triple6)] The rabbit does not see the mouse.[(triple10)] The rabbit is big.[(triple7)] The rabbit is blue.[(triple8)] The rabbit needs the mouse.[(triple9)] @1: The rabbit is cold.[(((triple4) -> rule5))] @2: The mouse is big.[(((triple4 ((triple4) -> rule5)) -> rule6))] @3: The mouse is nice.[(((((triple4 ((triple4) -> rule5)) -> rule6) triple2) -> rule3))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
((triple9) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
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 does not see the mouse.
("rabbit" "sees" "mouse" "-")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple9
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple4) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple4 ((triple4) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3