The cow chases the squirrel. The cow is green. The cow is kind. The cow is red. The cow does not see the mouse. The cow sees the squirrel. The mouse chases the squirrel. The mouse is green. The mouse likes the cow. The mouse likes the squirrel. The mouse sees the squirrel. The squirrel is not cold. The squirrel is kind. The squirrel likes the cow. The squirrel likes the mouse. The squirrel sees the mouse. If someone likes the mouse and the mouse does not chase the squirrel then the mouse does not see the cow. If the squirrel sees the mouse then the mouse is not red. If someone likes the mouse then the mouse is not cold. If someone is red and they do not see the squirrel then the squirrel likes the cow. If someone chases the squirrel then they like the squirrel. If someone is blue and not red then they like the cow.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is not cold.
("squirrel" "is" "cold" "-")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone likes the mouse and the mouse does not chase the squirrel then the mouse does not see the cow.
((("someone" "likes" "mouse" "+") ("mouse" "chases" "squirrel" "~")) -> ("mouse" "sees" "cow" "-"))
If the squirrel sees the mouse then the mouse is not red.
((("squirrel" "sees" "mouse" "+")) -> ("mouse" "is" "red" "-"))
If someone likes the mouse then the mouse is not cold.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "cold" "-"))
If someone is red and they do not see the squirrel then the squirrel likes the cow.
((("someone" "is" "red" "+") ("someone" "sees" "squirrel" "~")) -> ("squirrel" "likes" "cow" "+"))
If someone chases the squirrel then they like the squirrel.
((("someone" "chases" "squirrel" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone is blue and not red then they like the cow.
((("someone" "is" "blue" "+") ("someone" "is" "red" "~")) -> ("someone" "likes" "cow" "+"))
The mouse is green.
True
1
proof
[(triple8)]
("mouse" "is" "green" "+")
triple8
The mouse is not green.
False
1
inv-proof
[(triple8)]
("mouse" "is" "green" "-")
triple8
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow chases the squirrel.[(triple1)] The cow does not see the mouse.[(triple5)] The cow is green.[(triple2)] The cow is kind.[(triple3)] The cow is red.[(triple4)] The cow sees the squirrel.[(triple6)] The mouse chases the squirrel.[(triple7)] The mouse is green.[(triple8)] The mouse likes the cow.[(triple9)] The mouse likes the squirrel.[(triple10 OR ((triple7) -> rule5))] The mouse sees the squirrel.[(triple11)] The squirrel is kind.[(triple13)] The squirrel is not cold.[(triple12)] The squirrel likes the cow.[(triple14)] The squirrel likes the mouse.[(triple15)] The squirrel sees the mouse.[(triple16)] @1: The cow likes the squirrel.[(((triple1) -> rule5))] The mouse is not cold.[(((triple15) -> rule3))] The mouse is not red.[(((triple16) -> rule2))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
triple5
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple6
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple9
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple10
((triple7) -> (rule5 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple11
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple13
The squirrel is not cold.
("squirrel" "is" "cold" "-")
triple12
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple14
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple15
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple16
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
((triple1) -> (rule5 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The mouse is not cold.
("mouse" "is" "cold" "-")
((triple15) -> (rule3 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The mouse is not red.
("mouse" "is" "red" "-")
((triple16) -> (rule2 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1