The bear is not young. The cat visits the bear. The dog visits the bear. If the cat visits the bear and the dog does not visit the cat then the bear does not like the dog. If someone visits the bear and the bear visits the dog then they like the cat. If someone sees the cat and they are green then they see the dog. If someone visits the bear then the bear does not visit the cat. If someone likes the dog then they see the bear. If someone sees the cat and the cat does not see the bear then the bear likes the cat.
The bear is not young.
("bear" "is" "young" "-")
The cat visits the bear.
("cat" "visits" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
If the cat visits the bear and the dog does not visit the cat then the bear does not like the dog.
((("cat" "visits" "bear" "+") ("dog" "visits" "cat" "~")) -> ("bear" "likes" "dog" "-"))
If someone visits the bear and the bear visits the dog then they like the cat.
((("someone" "visits" "bear" "+") ("bear" "visits" "dog" "+")) -> ("someone" "likes" "cat" "+"))
If someone sees the cat and they are green then they see the dog.
((("someone" "sees" "cat" "+") ("someone" "is" "green" "+")) -> ("someone" "sees" "dog" "+"))
If someone visits the bear then the bear does not visit the cat.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "cat" "-"))
If someone likes the dog then they see the bear.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the cat and the cat does not see the bear then the bear likes the cat.
((("someone" "sees" "cat" "+") ("cat" "sees" "bear" "~")) -> ("bear" "likes" "cat" "+"))
The dog visits the bear.
True
1
proof
[(triple3)]
("dog" "visits" "bear" "+")
triple3
The bear is young.
False
1
inv-proof
[(triple1)]
("bear" "is" "young" "+")
triple1
The bear does not visit the cat.
True
2
proof
[(((triple2) -> rule4) OR ((triple3) -> rule4))]
("bear" "visits" "cat" "-")
((triple2) -> (rule4 % int1))
The bear does not visit the cat.
("bear" "visits" "cat" "-")
int1
((triple3) -> (rule4 % int1))
The bear does not visit the cat.
("bear" "visits" "cat" "-")
int1
The bear visits the cat.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple3) -> rule4))]
("bear" "visits" "cat" "+")
((triple2) -> (rule4 % int1))
The bear does not visit the cat.
("bear" "visits" "cat" "-")
int1
((triple3) -> (rule4 % int1))
The bear does not visit the cat.
("bear" "visits" "cat" "-")
int1
The bear does not see the dog.
Unknown
inv-rconc
[@1: The bear sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "dog" "-")
The cat sees the dog.
Unknown
rconc
[@1: The cat sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "dog" "+")
The cat does not like the dog.
Unknown
inv-random
[@0: The cat likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "dog" "-")
The dog visits the cat.
Unknown
random
[@0: The dog visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cat" "+")
@0: The bear is not young.[(triple1)] The cat visits the bear.[(triple2)] The dog visits the bear.[(triple3)] @1: The bear does not visit the cat.[(((triple2) -> rule4) OR ((triple3) -> rule4))]
The bear is not young.
("bear" "is" "young" "-")
triple1
The cat visits the bear.
("cat" "visits" "bear" "+")
triple2
The dog visits the bear.
("dog" "visits" "bear" "+")
triple3
The bear does not visit the cat.
("bear" "visits" "cat" "-")
((triple2) -> (rule4 % int1))
The bear does not visit the cat.
("bear" "visits" "cat" "-")
int1
((triple3) -> (rule4 % int1))
The bear does not visit the cat.
("bear" "visits" "cat" "-")
int1