The bear chases the rabbit. The bear is rough. The bear is young. The dog is not rough. The dog sees the rabbit. The rabbit is not red. The rabbit needs the bear. The rabbit does not need the dog. The rabbit sees the bear. The tiger chases the bear. The tiger is not blue. The tiger needs the bear. If someone is young then they do not see the tiger. If someone sees the rabbit then the rabbit chases the bear. If someone chases the bear and the bear needs the rabbit then they are not red. If someone is red and they do not see the dog then they do not chase the rabbit. If someone chases the dog and the dog needs the bear then they do not chase the tiger. If someone sees the bear and they are not red then they chase the dog.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The dog is not rough.
("dog" "is" "rough" "-")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If someone is young then they do not see the tiger.
((("someone" "is" "young" "+")) -> ("someone" "sees" "tiger" "-"))
If someone sees the rabbit then the rabbit chases the bear.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "chases" "bear" "+"))
If someone chases the bear and the bear needs the rabbit then they are not red.
((("someone" "chases" "bear" "+") ("bear" "needs" "rabbit" "+")) -> ("someone" "is" "red" "-"))
If someone is red and they do not see the dog then they do not chase the rabbit.
((("someone" "is" "red" "+") ("someone" "sees" "dog" "~")) -> ("someone" "chases" "rabbit" "-"))
If someone chases the dog and the dog needs the bear then they do not chase the tiger.
((("someone" "chases" "dog" "+") ("dog" "needs" "bear" "+")) -> ("someone" "chases" "tiger" "-"))
If someone sees the bear and they are not red then they chase the dog.
((("someone" "sees" "bear" "+") ("someone" "is" "red" "~")) -> ("someone" "chases" "dog" "+"))
The rabbit needs the bear.
True
1
proof
[(triple7)]
("rabbit" "needs" "bear" "+")
triple7
The tiger is blue.
False
1
inv-proof
[(triple11)]
("tiger" "is" "blue" "+")
triple11
The bear does not see the tiger.
True
2
proof
[(((triple3) -> rule1))]
("bear" "sees" "tiger" "-")
((triple3) -> (rule1 % int1))
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int1
The rabbit does not chase the dog.
False
3
inv-proof
[(((triple9 triple6) -> rule6))]
("rabbit" "chases" "dog" "-")
((triple9 triple6) -> (rule6 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The bear does not chase the dog.
Unknown
inv-rconc
[@1: The bear chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "chases" "dog" "-")
The tiger chases the dog.
Unknown
rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "dog" "+")
The rabbit does not see the tiger.
Unknown
inv-random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The bear chases the rabbit.[(triple1)] The bear is rough.[(triple2)] The bear is young.[(triple3)] The dog is not rough.[(triple4)] The dog sees the rabbit.[(triple5)] The rabbit does not need the dog.[(triple8)] The rabbit is not red.[(triple6)] The rabbit needs the bear.[(triple7)] The rabbit sees the bear.[(triple9)] The tiger chases the bear.[(triple10)] The tiger is not blue.[(triple11)] The tiger needs the bear.[(triple12)] @1: The bear does not see the tiger.[(((triple3) -> rule1))] The rabbit chases the bear.[(((triple5) -> rule2))] The rabbit chases the dog.[(((triple9 triple6) -> rule6))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The dog is not rough.
("dog" "is" "rough" "-")
triple4
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple5
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
triple8
The rabbit is not red.
("rabbit" "is" "red" "-")
triple6
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple7
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple9
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple10
The tiger is not blue.
("tiger" "is" "blue" "-")
triple11
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple12
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
((triple3) -> (rule1 % int1))
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple5) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((triple9 triple6) -> (rule6 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1