The bear sees the dog. The cat needs the dog. The dog is red. If someone is big and they visit the bear then the bear visits the cat. If someone sees the dog then the dog visits the cat. If someone needs the cat then the cat needs the bear.
The bear sees the dog.
("bear" "sees" "dog" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog is red.
("dog" "is" "red" "+")
If someone is big and they visit the bear then the bear visits the cat.
((("someone" "is" "big" "+") ("someone" "visits" "bear" "+")) -> ("bear" "visits" "cat" "+"))
If someone sees the dog then the dog visits the cat.
((("someone" "sees" "dog" "+")) -> ("dog" "visits" "cat" "+"))
If someone needs the cat then the cat needs the bear.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "bear" "+"))
The dog is red.
True
1
proof
[(triple3)]
("dog" "is" "red" "+")
triple3
The dog is not red.
False
1
inv-proof
[(triple3)]
("dog" "is" "red" "-")
triple3
The dog visits the cat.
True
2
proof
[(((triple1) -> rule2))]
("dog" "visits" "cat" "+")
((triple1) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "visits" "cat" "-")
((triple1) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The bear does not visit the cat.
Unknown
inv-rconc
[@1: The bear visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "cat" "-")
The cat needs the bear.
Unknown
rconc
[@1: The cat needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "bear" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear sees the dog.[(triple1)] The cat needs the dog.[(triple2)] The dog is red.[(triple3)] @1: The dog visits the cat.[(((triple1) -> rule2))]
The bear sees the dog.
("bear" "sees" "dog" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The dog visits the cat.
("dog" "visits" "cat" "+")
((triple1) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1