The bear needs the dog. The bear visits the dog. The dog needs the bear. If the dog eats the bear then the bear eats the dog. If something needs the bear then it does not visit the bear.
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
If the dog eats the bear then the bear eats the dog.
((("dog" "eats" "bear" "+")) -> ("bear" "eats" "dog" "+"))
If something needs the bear then it does not visit the bear.
((("something" "needs" "bear" "+")) -> ("something" "visits" "bear" "-"))
The dog needs the bear.
True
1
proof
[(triple3)]
("dog" "needs" "bear" "+")
triple3
The dog does not need the bear.
False
1
inv-proof
[(triple3)]
("dog" "needs" "bear" "-")
triple3
The dog does not visit the bear.
True
2
proof
[(((triple3) -> rule2))]
("dog" "visits" "bear" "-")
((triple3) -> (rule2 % int1))
The dog does not visit the bear.
("dog" "visits" "bear" "-")
int1
The dog visits the bear.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "visits" "bear" "+")
((triple3) -> (rule2 % int1))
The dog does not visit the bear.
("dog" "visits" "bear" "-")
int1
The bear does not eat the dog.
Unknown
inv-rconc
[@1: The bear eats the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "dog" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The bear needs the dog.[(triple1)] The bear visits the dog.[(triple2)] The dog needs the bear.[(triple3)] @1: The dog does not visit the bear.[(((triple3) -> rule2))]
The bear needs the dog.
("bear" "needs" "dog" "+")
triple1
The bear visits the dog.
("bear" "visits" "dog" "+")
triple2
The dog needs the bear.
("dog" "needs" "bear" "+")
triple3
The dog does not visit the bear.
("dog" "visits" "bear" "-")
((triple3) -> (rule2 % int1))
The dog does not visit the bear.
("dog" "visits" "bear" "-")
int1