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