The cat is not red. The cat visits the squirrel. The mouse is blue. The mouse sees the cat. The mouse sees the rabbit. The mouse visits the rabbit. The mouse does not visit the squirrel. The rabbit likes the cat. The rabbit likes the mouse. The rabbit likes the squirrel. The squirrel is rough. The squirrel does not like the rabbit. The squirrel does not see the cat. The squirrel sees the mouse. The squirrel visits the mouse. If something sees the squirrel and the squirrel is red then the squirrel is not blue. If something sees the cat then the cat is not round. If the rabbit is red and the rabbit likes the mouse then the rabbit does not see the mouse. If something is rough and it likes the mouse then the mouse is not big. If the squirrel visits the cat and the squirrel is big then the squirrel does not visit the rabbit. If something visits the rabbit then the rabbit sees the squirrel. If something likes the squirrel and it does not see the mouse then the squirrel likes the rabbit. If something is round and it does not like the rabbit then it does not visit the squirrel.
The cat is not red.
("cat" "is" "red" "-")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel does not like the rabbit.
("squirrel" "likes" "rabbit" "-")
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something sees the squirrel and the squirrel is red then the squirrel is not blue.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "red" "+")) -> ("squirrel" "is" "blue" "-"))
If something sees the cat then the cat is not round.
((("something" "sees" "cat" "+")) -> ("cat" "is" "round" "-"))
If the rabbit is red and the rabbit likes the mouse then the rabbit does not see the mouse.
((("rabbit" "is" "red" "+") ("rabbit" "likes" "mouse" "+")) -> ("rabbit" "sees" "mouse" "-"))
If something is rough and it likes the mouse then the mouse is not big.
((("something" "is" "rough" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "is" "big" "-"))
If the squirrel visits the cat and the squirrel is big then the squirrel does not visit the rabbit.
((("squirrel" "visits" "cat" "+") ("squirrel" "is" "big" "+")) -> ("squirrel" "visits" "rabbit" "-"))
If something visits the rabbit then the rabbit sees the squirrel.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If something likes the squirrel and it does not see the mouse then the squirrel likes the rabbit.
((("something" "likes" "squirrel" "+") ("something" "sees" "mouse" "~")) -> ("squirrel" "likes" "rabbit" "+"))
If something is round and it does not like the rabbit then it does not visit the squirrel.
((("something" "is" "round" "+") ("something" "likes" "rabbit" "~")) -> ("something" "visits" "squirrel" "-"))
The cat visits the squirrel.
True
1
proof
[(triple2)]
("cat" "visits" "squirrel" "+")
triple2
The mouse does not see the rabbit.
False
1
inv-proof
[(triple5)]
("mouse" "sees" "rabbit" "-")
triple5
The cat is not round.
True
2
proof
[(((triple4) -> rule2))]
("cat" "is" "round" "-")
((triple4) -> (rule2 % int1))
The cat is not round.
("cat" "is" "round" "-")
int1
The cat is round.
False
2
inv-proof
[(((triple4) -> rule2))]
("cat" "is" "round" "+")
((triple4) -> (rule2 % int1))
The cat is not round.
("cat" "is" "round" "-")
int1
The cat does not see the mouse.
Unknown
inv-random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "-")
The rabbit visits the mouse.
Unknown
random
[@0: The rabbit visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "mouse" "+")
The squirrel does not see the rabbit.
Unknown
inv-random
[@0: The squirrel sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "rabbit" "-")
The squirrel visits the rabbit.
Unknown
random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "+")
@0: The cat is not red.[(triple1)] The cat visits the squirrel.[(triple2)] The mouse does not visit the squirrel.[(triple7)] The mouse is blue.[(triple3)] The mouse sees the cat.[(triple4)] The mouse sees the rabbit.[(triple5)] The mouse visits the rabbit.[(triple6)] The rabbit likes the cat.[(triple8)] The rabbit likes the mouse.[(triple9)] The rabbit likes the squirrel.[(triple10)] The squirrel does not like the rabbit.[(triple12)] The squirrel does not see the cat.[(triple13)] The squirrel is rough.[(triple11)] The squirrel sees the mouse.[(triple14)] The squirrel visits the mouse.[(triple15)] @1: The cat is not round.[(((triple4) -> rule2))] The rabbit sees the squirrel.[(((triple6) -> rule6))]
The cat is not red.
("cat" "is" "red" "-")
triple1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple2
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple4
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple5
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple6
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple8
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple9
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple10
The squirrel does not like the rabbit.
("squirrel" "likes" "rabbit" "-")
triple12
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple14
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple15
The cat is not round.
("cat" "is" "round" "-")
((triple4) -> (rule2 % int1))
The cat is not round.
("cat" "is" "round" "-")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple6) -> (rule6 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1