The bear chases the dog. The bear is not rough. The bear sees the squirrel. The dog chases the squirrel. The dog is rough. The dog likes the bear. The dog sees the bear. The dog sees the squirrel. The dog sees the tiger. The squirrel chases the dog. The squirrel does not like the dog. The tiger does not chase the bear. The tiger likes the dog. The tiger sees the bear. The tiger does not see the squirrel. If someone sees the dog and they like the dog then the dog does not chase the tiger. If someone likes the dog then they see the dog. If someone is green then they like the squirrel. If the bear is round then the bear chases the dog. If someone sees the dog then the dog is rough. If the tiger is not green then the tiger is rough. If someone is green and they like the squirrel then they chase the squirrel. If someone likes the dog and they do not chase the dog then the dog likes the squirrel.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear is not rough.
("bear" "is" "rough" "-")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
If someone sees the dog and they like the dog then the dog does not chase the tiger.
((("someone" "sees" "dog" "+") ("someone" "likes" "dog" "+")) -> ("dog" "chases" "tiger" "-"))
If someone likes the dog then they see the dog.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "dog" "+"))
If someone is green then they like the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "likes" "squirrel" "+"))
If the bear is round then the bear chases the dog.
((("bear" "is" "round" "+")) -> ("bear" "chases" "dog" "+"))
If someone sees the dog then the dog is rough.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "rough" "+"))
If the tiger is not green then the tiger is rough.
((("tiger" "is" "green" "~")) -> ("tiger" "is" "rough" "+"))
If someone is green and they like the squirrel then they chase the squirrel.
((("someone" "is" "green" "+") ("someone" "likes" "squirrel" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone likes the dog and they do not chase the dog then the dog likes the squirrel.
((("someone" "likes" "dog" "+") ("someone" "chases" "dog" "~")) -> ("dog" "likes" "squirrel" "+"))
The bear is not rough.
True
1
proof
[(triple2)]
("bear" "is" "rough" "-")
triple2
The tiger does not see the bear.
False
1
inv-proof
[(triple14)]
("tiger" "sees" "bear" "-")
triple14
The tiger sees the dog.
True
2
proof
[(((triple13) -> rule2))]
("tiger" "sees" "dog" "+")
((triple13) -> (rule2 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger does not see the dog.
False
2
inv-proof
[(((triple13) -> rule2))]
("tiger" "sees" "dog" "-")
((triple13) -> (rule2 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The dog does not chase the tiger.
True
4
proof
[(((((triple13) -> rule2) triple13) -> rule1))]
("dog" "chases" "tiger" "-")
((((triple13) -> (rule2 % int2)) triple13) -> (rule1 % int1))
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The dog chases the tiger.
False
4
inv-proof
[(((((triple13) -> rule2) triple13) -> rule1))]
("dog" "chases" "tiger" "+")
((((triple13) -> (rule2 % int2)) triple13) -> (rule1 % int1))
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The bear does not like the squirrel.
Unknown
inv-rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "likes" "squirrel" "-")
The tiger likes the squirrel.
Unknown
rconc
[@1: The tiger likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "squirrel" "+")
The squirrel does not see the dog.
Unknown
inv-rconc
[@1: The squirrel sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "dog" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The squirrel does not like the tiger.
Unknown
inv-random
[@0: The squirrel likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "tiger" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The bear chases the dog.[(triple1)] The bear is not rough.[(triple2)] The bear sees the squirrel.[(triple3)] The dog chases the squirrel.[(triple4)] The dog is rough.[(triple5 OR ((((triple13) -> rule2)) -> rule5))] The dog likes the bear.[(triple6)] The dog sees the bear.[(triple7)] The dog sees the squirrel.[(triple8)] The dog sees the tiger.[(triple9)] The squirrel chases the dog.[(triple10)] The squirrel does not like the dog.[(triple11)] The tiger does not chase the bear.[(triple12)] The tiger does not see the squirrel.[(triple15)] The tiger likes the dog.[(triple13)] The tiger sees the bear.[(triple14)] @1: The tiger sees the dog.[(((triple13) -> rule2))] @2: The dog does not chase the tiger.[(((((triple13) -> rule2) triple13) -> rule1))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear is not rough.
("bear" "is" "rough" "-")
triple2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
((((triple13) -> (rule2 % int2))) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
triple6
The dog sees the bear.
("dog" "sees" "bear" "+")
triple7
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple8
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple9
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple10
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
triple11
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
triple12
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
triple15
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple13
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple14
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((triple13) -> (rule2 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
((((triple13) -> (rule2 % int2)) triple13) -> (rule1 % int1))
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2