The bear is red. The bear needs the dog. The bear does not see the dog. The bear sees the mouse. The dog is big. The dog is red. The mouse likes the squirrel. The mouse sees the squirrel. The squirrel is round. The squirrel needs the dog. The squirrel sees the bear. The squirrel sees the dog. If something needs the dog then it likes the squirrel. All big things are nice. If the mouse needs the bear then the mouse is blue. If something is big and nice then it needs the dog. If something needs the mouse and the mouse needs the bear then the bear sees the mouse. If the dog does not like the squirrel then the dog does not need the squirrel.
The bear is red.
("bear" "is" "red" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear does not see the dog.
("bear" "sees" "dog" "-")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If something needs the dog then it likes the squirrel.
((("something" "needs" "dog" "+")) -> ("something" "likes" "squirrel" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If the mouse needs the bear then the mouse is blue.
((("mouse" "needs" "bear" "+")) -> ("mouse" "is" "blue" "+"))
If something is big and nice then it needs the dog.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "needs" "dog" "+"))
If something needs the mouse and the mouse needs the bear then the bear sees the mouse.
((("something" "needs" "mouse" "+") ("mouse" "needs" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If the dog does not like the squirrel then the dog does not need the squirrel.
((("dog" "likes" "squirrel" "~")) -> ("dog" "needs" "squirrel" "-"))
The squirrel sees the bear.
True
1
proof
[(triple11)]
("squirrel" "sees" "bear" "+")
triple11
The mouse does not like the squirrel.
False
1
inv-proof
[(triple7)]
("mouse" "likes" "squirrel" "-")
triple7
The dog is nice.
True
2
proof
[(((triple5) -> rule2))]
("dog" "is" "nice" "+")
((triple5) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The squirrel does not like the squirrel.
False
2
inv-proof
[(((triple10) -> rule1))]
("squirrel" "likes" "squirrel" "-")
((triple10) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The dog needs the dog.
True
4
proof
[(((triple5 ((triple5) -> rule2)) -> rule4))]
("dog" "needs" "dog" "+")
((triple5 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog does not need the dog.
False
4
inv-proof
[(((triple5 ((triple5) -> rule2)) -> rule4))]
("dog" "needs" "dog" "-")
((triple5 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog likes the squirrel.
True
5
proof
[(((((triple5 ((triple5) -> rule2)) -> rule4)) -> rule1))]
("dog" "likes" "squirrel" "+")
((((triple5 ((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog does not like the squirrel.
False
5
inv-proof
[(((((triple5 ((triple5) -> rule2)) -> rule4)) -> rule1))]
("dog" "likes" "squirrel" "-")
((((triple5 ((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "blue" "-")
The bear is nice.
Unknown
rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "nice" "+")
The mouse does not need the dog.
Unknown
inv-rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "dog" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "nice" "+")
The dog does not like the mouse.
Unknown
inv-random
[@0: The dog likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "mouse" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse needs the bear.
Unknown
random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "+")
@0: The bear does not see the dog.[(triple3)] The bear is red.[(triple1)] The bear needs the dog.[(triple2)] The bear sees the mouse.[(triple4)] The dog is big.[(triple5)] The dog is red.[(triple6)] The mouse likes the squirrel.[(triple7)] The mouse sees the squirrel.[(triple8)] The squirrel is round.[(triple9)] The squirrel needs the dog.[(triple10)] The squirrel sees the bear.[(triple11)] The squirrel sees the dog.[(triple12)] @1: The bear likes the squirrel.[(((triple2) -> rule1))] The dog is nice.[(((triple5) -> rule2))] The squirrel likes the squirrel.[(((triple10) -> rule1))] @2: The dog needs the dog.[(((triple5 ((triple5) -> rule2)) -> rule4))] @3: The dog likes the squirrel.[(((((triple5 ((triple5) -> rule2)) -> rule4)) -> rule1))]
The bear does not see the dog.
("bear" "sees" "dog" "-")
triple3
The bear is red.
("bear" "is" "red" "+")
triple1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple7
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple10
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple11
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple12
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((triple2) -> (rule1 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple5) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple10) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple5 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((((triple5 ((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3