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