The bear is nice. The bear visits the dog. The dog needs the bear. If someone is green and they like the dog then they are round. If the dog needs the bear and the dog likes the bear then the dog visits the bear. If someone visits the dog then they need the dog. If the bear likes the dog and the dog needs the bear then the dog is nice. If someone needs the dog then the dog is green. If someone needs the dog and they need the bear then the bear is young. If someone needs the bear and the bear visits the dog then they need the dog. If someone likes the dog then they visit the bear.
The bear is nice.
("bear" "is" "nice" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
If someone is green and they like the dog then they are round.
((("someone" "is" "green" "+") ("someone" "likes" "dog" "+")) -> ("someone" "is" "round" "+"))
If the dog needs the bear and the dog likes the bear then the dog visits the bear.
((("dog" "needs" "bear" "+") ("dog" "likes" "bear" "+")) -> ("dog" "visits" "bear" "+"))
If someone visits the dog then they need the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "needs" "dog" "+"))
If the bear likes the dog and the dog needs the bear then the dog is nice.
((("bear" "likes" "dog" "+") ("dog" "needs" "bear" "+")) -> ("dog" "is" "nice" "+"))
If someone needs the dog then the dog is green.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "green" "+"))
If someone needs the dog and they need the bear then the bear is young.
((("someone" "needs" "dog" "+") ("someone" "needs" "bear" "+")) -> ("bear" "is" "young" "+"))
If someone needs the bear and the bear visits the dog then they need the dog.
((("someone" "needs" "bear" "+") ("bear" "visits" "dog" "+")) -> ("someone" "needs" "dog" "+"))
If someone likes the dog then they visit the bear.
((("someone" "likes" "dog" "+")) -> ("someone" "visits" "bear" "+"))
The bear is nice.
True
1
proof
[(triple1)]
("bear" "is" "nice" "+")
triple1
The bear is not nice.
False
1
inv-proof
[(triple1)]
("bear" "is" "nice" "-")
triple1
The bear needs the dog.
True
2
proof
[(((triple2) -> rule3))]
("bear" "needs" "dog" "+")
((triple2) -> (rule3 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The dog does not need the dog.
False
3
inv-proof
[(((triple3 triple2) -> rule7))]
("dog" "needs" "dog" "-")
((triple3 triple2) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is green.
True
3
proof
[(((((triple2) -> rule3)) -> rule5) OR ((((triple3 triple2) -> rule7)) -> rule5))]
("dog" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
((((triple3 triple2) -> (rule7 % int2))) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is not green.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5) OR ((((triple3 triple2) -> rule7)) -> rule5))]
("dog" "is" "green" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
((((triple3 triple2) -> (rule7 % int2))) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "round" "-")
The dog visits the bear.
Unknown
rconc
[@1: The dog visits the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "bear" "+")
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "nice" "-")
The bear likes the dog.
Unknown
random
[@0: The bear likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "dog" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The bear is nice.[(triple1)] The bear visits the dog.[(triple2)] The dog needs the bear.[(triple3)] @1: The bear needs the dog.[(((triple2) -> rule3))] The dog needs the dog.[(((triple3 triple2) -> rule7))] @2: The bear is young.[(((((triple3 triple2) -> rule7) triple3) -> rule6))] The dog is green.[(((((triple2) -> rule3)) -> rule5) OR ((((triple3 triple2) -> rule7)) -> rule5))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear visits the dog.
("bear" "visits" "dog" "+")
triple2
The dog needs the bear.
("dog" "needs" "bear" "+")
triple3
The bear needs the dog.
("bear" "needs" "dog" "+")
((triple2) -> (rule3 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple3 triple2) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The bear is young.
("bear" "is" "young" "+")
((((triple3 triple2) -> (rule7 % int2)) triple3) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is green.
("dog" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
((((triple3 triple2) -> (rule7 % int2))) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2