The dog is blue. The dog needs the mouse. The mouse is not kind. The mouse is round. The mouse likes the squirrel. The mouse needs the squirrel. The squirrel is not blue. The squirrel is not nice. The squirrel is young. The squirrel does not like the dog. The squirrel likes the mouse. The squirrel sees the dog. If someone sees the dog then they are not nice. If someone needs the mouse then the mouse is nice. If someone is blue and kind then they need the mouse. If someone likes the mouse then the mouse sees the squirrel. If someone needs the dog then they do not like the dog. If someone sees the mouse and the mouse does not like the dog then the dog sees the squirrel. If someone sees the dog and the dog is young then the dog does not see the squirrel. If someone sees the squirrel then the squirrel does not see the mouse.
The dog is blue.
("dog" "is" "blue" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse is not kind.
("mouse" "is" "kind" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel is not blue.
("squirrel" "is" "blue" "-")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If someone sees the dog then they are not nice.
((("someone" "sees" "dog" "+")) -> ("someone" "is" "nice" "-"))
If someone needs the mouse then the mouse is nice.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If someone is blue and kind then they need the mouse.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "needs" "mouse" "+"))
If someone likes the mouse then the mouse sees the squirrel.
((("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
If someone needs the dog then they do not like the dog.
((("someone" "needs" "dog" "+")) -> ("someone" "likes" "dog" "-"))
If someone sees the mouse and the mouse does not like the dog then the dog sees the squirrel.
((("someone" "sees" "mouse" "+") ("mouse" "likes" "dog" "~")) -> ("dog" "sees" "squirrel" "+"))
If someone sees the dog and the dog is young then the dog does not see the squirrel.
((("someone" "sees" "dog" "+") ("dog" "is" "young" "+")) -> ("dog" "sees" "squirrel" "-"))
If someone sees the squirrel then the squirrel does not see the mouse.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "mouse" "-"))
The squirrel is not nice.
True
1
proof
[(triple8 OR ((triple12) -> rule1))]
("squirrel" "is" "nice" "-")
triple8
((triple12) -> (rule1 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The dog does not need the mouse.
False
1
inv-proof
[(triple2)]
("dog" "needs" "mouse" "-")
triple2
The mouse sees the squirrel.
True
2
proof
[(((triple11) -> rule4))]
("mouse" "sees" "squirrel" "+")
((triple11) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse does not see the squirrel.
False
2
inv-proof
[(((triple11) -> rule4))]
("mouse" "sees" "squirrel" "-")
((triple11) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel does not see the mouse.
True
3
proof
[(((((triple11) -> rule4)) -> rule8))]
("squirrel" "sees" "mouse" "-")
((((triple11) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The squirrel sees the mouse.
False
3
inv-proof
[(((((triple11) -> rule4)) -> rule8))]
("squirrel" "sees" "mouse" "+")
((((triple11) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The dog does not see the squirrel.
Unknown
inv-rconc
[@1: The dog sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "squirrel" "-")
The squirrel needs the mouse.
Unknown
rconc
[@1: The squirrel needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "needs" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse sees the dog.
Unknown
random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "+")
The dog does not need the squirrel.
Unknown
inv-random
[@0: The dog needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The dog is blue.[(triple1)] The dog needs the mouse.[(triple2)] The mouse is not kind.[(triple3)] The mouse is round.[(triple4)] The mouse likes the squirrel.[(triple5)] The mouse needs the squirrel.[(triple6)] The squirrel does not like the dog.[(triple10)] The squirrel is not blue.[(triple7)] The squirrel is not nice.[(triple8 OR ((triple12) -> rule1))] The squirrel is young.[(triple9)] The squirrel likes the mouse.[(triple11)] The squirrel sees the dog.[(triple12)] @1: The mouse is nice.[(((triple2) -> rule2))] The mouse sees the squirrel.[(((triple11) -> rule4))] @2: The squirrel does not see the mouse.[(((((triple11) -> rule4)) -> rule8))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple2
The mouse is not kind.
("mouse" "is" "kind" "-")
triple3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple5
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple6
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
triple10
The squirrel is not blue.
("squirrel" "is" "blue" "-")
triple7
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple8
((triple12) -> (rule1 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
triple9
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple11
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple12
The mouse is nice.
("mouse" "is" "nice" "+")
((triple2) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple11) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
((((triple11) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2