The mouse chases the squirrel. The mouse is big. The mouse is cold. The mouse is red. The mouse is rough. The mouse visits the squirrel. The squirrel chases the mouse. The squirrel is big. The squirrel is cold. The squirrel is round. The squirrel likes the mouse. The squirrel visits the mouse. If someone visits the mouse and the mouse likes the squirrel then the mouse is cold. If someone is round then they visit the squirrel. If someone likes the mouse and the mouse is round then they are round. If someone visits the mouse and the mouse is round then they are round. If someone visits the squirrel and the squirrel is round then they like the squirrel. If someone visits the mouse then the mouse visits the squirrel. Red people are big. If someone visits the squirrel then they chase the mouse.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone visits the mouse and the mouse likes the squirrel then the mouse is cold.
((("someone" "visits" "mouse" "+") ("mouse" "likes" "squirrel" "+")) -> ("mouse" "is" "cold" "+"))
If someone is round then they visit the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone likes the mouse and the mouse is round then they are round.
((("someone" "likes" "mouse" "+") ("mouse" "is" "round" "+")) -> ("someone" "is" "round" "+"))
If someone visits the mouse and the mouse is round then they are round.
((("someone" "visits" "mouse" "+") ("mouse" "is" "round" "+")) -> ("someone" "is" "round" "+"))
If someone visits the squirrel and the squirrel is round then they like the squirrel.
((("someone" "visits" "squirrel" "+") ("squirrel" "is" "round" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone visits the mouse then the mouse visits the squirrel.
((("someone" "visits" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone visits the squirrel then they chase the mouse.
((("someone" "visits" "squirrel" "+")) -> ("someone" "chases" "mouse" "+"))
The squirrel likes the mouse.
True
1
proof
[(triple11)]
("squirrel" "likes" "mouse" "+")
triple11
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple12)]
("squirrel" "visits" "mouse" "-")
triple12
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "round" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The mouse chases the squirrel.[(triple1)] The mouse is big.[(triple2 OR ((triple4) -> rule7))] The mouse is cold.[(triple3 OR ((triple12 ((triple6 triple10) -> rule5)) -> rule1) OR ((triple12 ((((triple12) -> rule6) triple10) -> rule5)) -> rule1))] The mouse is red.[(triple4)] The mouse is rough.[(triple5)] The mouse visits the squirrel.[(triple6 OR ((triple12) -> rule6))] The squirrel chases the mouse.[(triple7 OR ((((triple10) -> rule2)) -> rule8))] The squirrel is big.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is round.[(triple10)] The squirrel likes the mouse.[(triple11)] The squirrel visits the mouse.[(triple12)] @1: The mouse chases the mouse.[(((triple6) -> rule8) OR ((((triple12) -> rule6)) -> rule8))] The mouse likes the squirrel.[(((triple6 triple10) -> rule5) OR ((((triple12) -> rule6) triple10) -> rule5))] The squirrel visits the squirrel.[(((triple10) -> rule2))] @2: The squirrel likes the squirrel.[(((((triple10) -> rule2) triple10) -> rule5))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
((triple4) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
((triple12 ((triple6 triple10) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
((triple12 ((((triple12) -> (rule6 % int3)) triple10) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple6
((triple12) -> (rule6 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple7
((((triple10) -> (rule2 % int2))) -> (rule8 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is round.
("squirrel" "is" "round" "+")
triple10
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple11
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple12
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple6) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
((triple6 triple10) -> (rule5 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
((((triple12) -> (rule6 % int2)) triple10) -> (rule5 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple10) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((triple10) -> (rule2 % int2)) triple10) -> (rule5 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2