The bear is red. The bear needs the dog. The dog eats the squirrel. The dog is big. The dog is red. The dog needs the bear. The dog sees the bear. The squirrel eats the tiger. The tiger eats the bear. The tiger is nice. The tiger is rough. The tiger sees the bear. If something is nice and rough then it does not see the dog.
The bear is red.
("bear" "is" "red" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something is nice and rough then it does not see the dog.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "sees" "dog" "-"))
The dog is big.
True
1
proof
[(triple4)]
("dog" "is" "big" "+")
triple4
The tiger does not see the bear.
False
1
inv-proof
[(triple12)]
("tiger" "sees" "bear" "-")
triple12
The tiger does not see the dog.
True
3
proof
[(((triple10 triple11) -> rule1))]
("tiger" "sees" "dog" "-")
((triple10 triple11) -> (rule1 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1
The tiger sees the dog.
False
3
inv-proof
[(((triple10 triple11) -> rule1))]
("tiger" "sees" "dog" "+")
((triple10 triple11) -> (rule1 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The bear eats the squirrel.
Unknown
random
[@0: The bear eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "squirrel" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The bear is red.[(triple1)] The bear needs the dog.[(triple2)] The dog eats the squirrel.[(triple3)] The dog is big.[(triple4)] The dog is red.[(triple5)] The dog needs the bear.[(triple6)] The dog sees the bear.[(triple7)] The squirrel eats the tiger.[(triple8)] The tiger eats the bear.[(triple9)] The tiger is nice.[(triple10)] The tiger is rough.[(triple11)] The tiger sees the bear.[(triple12)] @1: The tiger does not see the dog.[(((triple10 triple11) -> rule1))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple3
The dog is big.
("dog" "is" "big" "+")
triple4
The dog is red.
("dog" "is" "red" "+")
triple5
The dog needs the bear.
("dog" "needs" "bear" "+")
triple6
The dog sees the bear.
("dog" "sees" "bear" "+")
triple7
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple8
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple12
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
((triple10 triple11) -> (rule1 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1