The bear is big. The bear does not need the dog. The bear does not visit the cat. The cat chases the bear. The cat needs the dog. The dog needs the cat. The dog visits the bear. If someone visits the cat then they chase the dog. If someone is big and they do not visit the cat then they chase the dog. If someone visits the bear and the bear visits the dog then they do not chase the cat. If someone chases the cat then they are not blue. If someone visits the dog and they chase the dog then the dog visits the bear. If someone chases the dog and they do not visit the bear then they are rough.
The bear is big.
("bear" "is" "big" "+")
The bear does not need the dog.
("bear" "needs" "dog" "-")
The bear does not visit the cat.
("bear" "visits" "cat" "-")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
If someone visits the cat then they chase the dog.
((("someone" "visits" "cat" "+")) -> ("someone" "chases" "dog" "+"))
If someone is big and they do not visit the cat then they chase the dog.
((("someone" "is" "big" "+") ("someone" "visits" "cat" "~")) -> ("someone" "chases" "dog" "+"))
If someone visits the bear and the bear visits the dog then they do not chase the cat.
((("someone" "visits" "bear" "+") ("bear" "visits" "dog" "+")) -> ("someone" "chases" "cat" "-"))
If someone chases the cat then they are not blue.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "blue" "-"))
If someone visits the dog and they chase the dog then the dog visits the bear.
((("someone" "visits" "dog" "+") ("someone" "chases" "dog" "+")) -> ("dog" "visits" "bear" "+"))
If someone chases the dog and they do not visit the bear then they are rough.
((("someone" "chases" "dog" "+") ("someone" "visits" "bear" "~")) -> ("someone" "is" "rough" "+"))
The dog visits the bear.
True
1
proof
[(triple7)]
("dog" "visits" "bear" "+")
triple7
The dog does not need the cat.
False
1
inv-proof
[(triple6)]
("dog" "needs" "cat" "-")
triple6
The bear chases the dog.
True
3
proof
[(((triple1 triple3) -> rule2))]
("bear" "chases" "dog" "+")
((triple1 triple3) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The bear does not chase the dog.
False
3
inv-proof
[(((triple1 triple3) -> rule2))]
("bear" "chases" "dog" "-")
((triple1 triple3) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "rough" "-")
The dog is rough.
Unknown
rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "rough" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The bear does not need the dog.[(triple2)] The bear does not visit the cat.[(triple3)] The bear is big.[(triple1)] The cat chases the bear.[(triple4)] The cat needs the dog.[(triple5)] The dog needs the cat.[(triple6)] The dog visits the bear.[(triple7)] @1: The bear chases the dog.[(((triple1 triple3) -> rule2))]
The bear does not need the dog.
("bear" "needs" "dog" "-")
triple2
The bear does not visit the cat.
("bear" "visits" "cat" "-")
triple3
The bear is big.
("bear" "is" "big" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple4
The cat needs the dog.
("cat" "needs" "dog" "+")
triple5
The dog needs the cat.
("dog" "needs" "cat" "+")
triple6
The dog visits the bear.
("dog" "visits" "bear" "+")
triple7
The bear chases the dog.
("bear" "chases" "dog" "+")
((triple1 triple3) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1