The mouse eats the rabbit. The mouse likes the squirrel. The rabbit eats the mouse. The rabbit is green. The rabbit is not kind. The rabbit does not like the mouse. The rabbit likes the squirrel. The rabbit needs the mouse. The squirrel eats the mouse. The squirrel is blue. If something eats the mouse then the mouse needs the rabbit. If something needs the mouse and it is not kind then the mouse is blue. If something eats the squirrel and it does not need the squirrel then the squirrel eats the mouse. If the mouse is blue then the mouse likes the rabbit. If something likes the rabbit then the rabbit does not eat the squirrel. If the rabbit likes the squirrel and the rabbit is blue then the rabbit eats the squirrel.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is not kind.
("rabbit" "is" "kind" "-")
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If something eats the mouse then the mouse needs the rabbit.
((("something" "eats" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If something needs the mouse and it is not kind then the mouse is blue.
((("something" "needs" "mouse" "+") ("something" "is" "kind" "~")) -> ("mouse" "is" "blue" "+"))
If something eats the squirrel and it does not need the squirrel then the squirrel eats the mouse.
((("something" "eats" "squirrel" "+") ("something" "needs" "squirrel" "~")) -> ("squirrel" "eats" "mouse" "+"))
If the mouse is blue then the mouse likes the rabbit.
((("mouse" "is" "blue" "+")) -> ("mouse" "likes" "rabbit" "+"))
If something likes the rabbit then the rabbit does not eat the squirrel.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "eats" "squirrel" "-"))
If the rabbit likes the squirrel and the rabbit is blue then the rabbit eats the squirrel.
((("rabbit" "likes" "squirrel" "+") ("rabbit" "is" "blue" "+")) -> ("rabbit" "eats" "squirrel" "+"))
The mouse likes the squirrel.
True
1
proof
[(triple2)]
("mouse" "likes" "squirrel" "+")
triple2
The rabbit is kind.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "kind" "+")
triple5
The mouse needs the rabbit.
True
2
proof
[(((triple3) -> rule1) OR ((triple9) -> rule1))]
("mouse" "needs" "rabbit" "+")
((triple3) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple9) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse does not need the rabbit.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple9) -> rule1))]
("mouse" "needs" "rabbit" "-")
((triple3) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple9) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse likes the rabbit.
True
4
proof
[(((((triple8 triple5) -> rule2)) -> rule4))]
("mouse" "likes" "rabbit" "+")
((((triple8 triple5) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse does not like the rabbit.
False
4
inv-proof
[(((((triple8 triple5) -> rule2)) -> rule4))]
("mouse" "likes" "rabbit" "-")
((((triple8 triple5) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The rabbit does not eat the squirrel.
True
5
proof
[(((((((triple8 triple5) -> rule2)) -> rule4)) -> rule5))]
("rabbit" "eats" "squirrel" "-")
((((((triple8 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not eat the squirrel.
("rabbit" "eats" "squirrel" "-")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The rabbit eats the squirrel.
False
5
inv-proof
[(((((((triple8 triple5) -> rule2)) -> rule4)) -> rule5))]
("rabbit" "eats" "squirrel" "+")
((((((triple8 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not eat the squirrel.
("rabbit" "eats" "squirrel" "-")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not need the mouse.
Unknown
inv-random
[@0: The squirrel needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "mouse" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel likes the rabbit.
Unknown
random
[@0: The squirrel likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "rabbit" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The mouse eats the rabbit.[(triple1)] The mouse likes the squirrel.[(triple2)] The rabbit does not like the mouse.[(triple6)] The rabbit eats the mouse.[(triple3)] The rabbit is green.[(triple4)] The rabbit is not kind.[(triple5)] The rabbit likes the squirrel.[(triple7)] The rabbit needs the mouse.[(triple8)] The squirrel eats the mouse.[(triple9)] The squirrel is blue.[(triple10)] @1: The mouse is blue.[(((triple8 triple5) -> rule2))] The mouse needs the rabbit.[(((triple3) -> rule1) OR ((triple9) -> rule1))] @2: The mouse likes the rabbit.[(((((triple8 triple5) -> rule2)) -> rule4))] @3: The rabbit does not eat the squirrel.[(((((((triple8 triple5) -> rule2)) -> rule4)) -> rule5))]
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple2
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
triple6
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple3
The rabbit is green.
("rabbit" "is" "green" "+")
triple4
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple5
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple7
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple8
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The mouse is blue.
("mouse" "is" "blue" "+")
((triple8 triple5) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((triple3) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple9) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple8 triple5) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The rabbit does not eat the squirrel.
("rabbit" "eats" "squirrel" "-")
((((((triple8 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not eat the squirrel.
("rabbit" "eats" "squirrel" "-")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3