The cat eats the mouse. The cat is green. The cat is red. The cat is round. The cat needs the mouse. The cat needs the rabbit. The cat sees the rabbit. The mouse is blue. The mouse needs the rabbit. The mouse needs the squirrel. The mouse sees the rabbit. The rabbit is round. The squirrel is blue. The squirrel is red. The squirrel needs the cat. The squirrel needs the rabbit. If the squirrel is rough then the squirrel sees the rabbit. If someone is round then they see the rabbit. If someone needs the rabbit and they need the squirrel then the rabbit is blue. If someone is green and they see the squirrel then they see the rabbit. If the cat sees the rabbit and the cat eats the mouse then the cat is rough. If someone sees the cat then the cat sees the rabbit. If someone is green then they need the cat. If someone eats the mouse and they need the squirrel then they see the cat.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If the squirrel is rough then the squirrel sees the rabbit.
((("squirrel" "is" "rough" "+")) -> ("squirrel" "sees" "rabbit" "+"))
If someone is round then they see the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone needs the rabbit and they need the squirrel then the rabbit is blue.
((("someone" "needs" "rabbit" "+") ("someone" "needs" "squirrel" "+")) -> ("rabbit" "is" "blue" "+"))
If someone is green and they see the squirrel then they see the rabbit.
((("someone" "is" "green" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "rabbit" "+"))
If the cat sees the rabbit and the cat eats the mouse then the cat is rough.
((("cat" "sees" "rabbit" "+") ("cat" "eats" "mouse" "+")) -> ("cat" "is" "rough" "+"))
If someone sees the cat then the cat sees the rabbit.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "rabbit" "+"))
If someone is green then they need the cat.
((("someone" "is" "green" "+")) -> ("someone" "needs" "cat" "+"))
If someone eats the mouse and they need the squirrel then they see the cat.
((("someone" "eats" "mouse" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "sees" "cat" "+"))
The squirrel needs the rabbit.
True
1
proof
[(triple16)]
("squirrel" "needs" "rabbit" "+")
triple16
The cat does not see the rabbit.
False
1
inv-proof
[(triple7 OR ((triple4) -> rule2))]
("cat" "sees" "rabbit" "-")
triple7
((triple4) -> (rule2 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The rabbit is blue.
True
3
proof
[(((triple9 triple10) -> rule3))]
("rabbit" "is" "blue" "+")
((triple9 triple10) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple2) -> rule7))]
("cat" "needs" "cat" "-")
((triple2) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "sees" "cat" "-")
The squirrel sees the rabbit.
Unknown
rconc
[@1: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "rabbit" "+")
The cat does not see the squirrel.
Unknown
inv-random
[@0: The cat sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "squirrel" "-")
The squirrel eats the rabbit.
Unknown
random
[@0: The squirrel eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "rabbit" "+")
@0: The cat eats the mouse.[(triple1)] The cat is green.[(triple2)] The cat is red.[(triple3)] The cat is round.[(triple4)] The cat needs the mouse.[(triple5)] The cat needs the rabbit.[(triple6)] The cat sees the rabbit.[(triple7 OR ((triple4) -> rule2))] The mouse is blue.[(triple8)] The mouse needs the rabbit.[(triple9)] The mouse needs the squirrel.[(triple10)] The mouse sees the rabbit.[(triple11)] The rabbit is round.[(triple12)] The squirrel is blue.[(triple13)] The squirrel is red.[(triple14)] The squirrel needs the cat.[(triple15)] The squirrel needs the rabbit.[(triple16)] @1: The cat is rough.[(((triple7 triple1) -> rule5) OR ((((triple4) -> rule2) triple1) -> rule5))] The cat needs the cat.[(((triple2) -> rule7))] The rabbit is blue.[(((triple9 triple10) -> rule3))] The rabbit sees the rabbit.[(((triple12) -> rule2))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple7
((triple4) -> (rule2 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple9
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple10
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple11
The rabbit is round.
("rabbit" "is" "round" "+")
triple12
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple13
The squirrel is red.
("squirrel" "is" "red" "+")
triple14
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple15
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple16
The cat is rough.
("cat" "is" "rough" "+")
((triple7 triple1) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((((triple4) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple2) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple9 triple10) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple12) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1