The bear needs the mouse. The bear sees the squirrel. The dog is kind. The dog is red. The dog likes the bear. The dog needs the squirrel. The mouse is round. The mouse needs the dog. The mouse does not need the squirrel. The mouse sees the bear. The mouse does not see the squirrel. The squirrel does not need the mouse. If someone sees the squirrel then they see the bear.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
If someone sees the squirrel then they see the bear.
((("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "bear" "+"))
The mouse sees the bear.
True
1
proof
[(triple10)]
("mouse" "sees" "bear" "+")
triple10
The bear does not see the squirrel.
False
1
inv-proof
[(triple2)]
("bear" "sees" "squirrel" "-")
triple2
The bear sees the bear.
True
2
proof
[(((triple2) -> rule1))]
("bear" "sees" "bear" "+")
((triple2) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear does not see the bear.
False
2
inv-proof
[(((triple2) -> rule1))]
("bear" "sees" "bear" "-")
((triple2) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The squirrel does not see the bear.
Unknown
inv-rconc
[@1: The squirrel sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "bear" "-")
The dog sees the bear.
Unknown
rconc
[@1: The dog sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "bear" "+")
The dog does not see the squirrel.
Unknown
inv-random
[@0: The dog sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "squirrel" "-")
The squirrel sees the dog.
Unknown
random
[@0: The squirrel sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "dog" "+")
@0: The bear needs the mouse.[(triple1)] The bear sees the squirrel.[(triple2)] The dog is kind.[(triple3)] The dog is red.[(triple4)] The dog likes the bear.[(triple5)] The dog needs the squirrel.[(triple6)] The mouse does not need the squirrel.[(triple9)] The mouse does not see the squirrel.[(triple11)] The mouse is round.[(triple7)] The mouse needs the dog.[(triple8)] The mouse sees the bear.[(triple10)] The squirrel does not need the mouse.[(triple12)] @1: The bear sees the bear.[(((triple2) -> rule1))]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog likes the bear.
("dog" "likes" "bear" "+")
triple5
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple6
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
triple9
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
triple11
The mouse is round.
("mouse" "is" "round" "+")
triple7
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple8
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple10
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
triple12
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple2) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1