The mouse chases the rabbit. The mouse is rough. The mouse is young. The rabbit chases the mouse. The rabbit eats the mouse. The rabbit is big. The rabbit is cold. The rabbit is rough. The rabbit is young. The rabbit needs the mouse. If someone is young then they eat the mouse. Rough people are cold.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If someone is young then they eat the mouse.
((("someone" "is" "young" "+")) -> ("someone" "eats" "mouse" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
The rabbit is rough.
True
1
proof
[(triple8)]
("rabbit" "is" "rough" "+")
triple8
The rabbit does not need the mouse.
False
1
inv-proof
[(triple10)]
("rabbit" "needs" "mouse" "-")
triple10
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse chases the rabbit.[(triple1)] The mouse is rough.[(triple2)] The mouse is young.[(triple3)] The rabbit chases the mouse.[(triple4)] The rabbit eats the mouse.[(triple5 OR ((triple9) -> rule1))] The rabbit is big.[(triple6)] The rabbit is cold.[(triple7 OR ((triple8) -> rule2))] The rabbit is rough.[(triple8)] The rabbit is young.[(triple9)] The rabbit needs the mouse.[(triple10)] @1: The mouse eats the mouse.[(((triple3) -> rule1))] The mouse is cold.[(((triple2) -> rule2))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple4
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple5
((triple9) -> (rule1 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple6
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple7
((triple8) -> (rule2 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit is young.
("rabbit" "is" "young" "+")
triple9
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple10
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple3) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple2) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1