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