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