The bear does not like the dog. The dog is nice. If something likes the dog then it is green. If something is cold and it eats the bear then the bear sees the dog. If something is nice then it sees the bear. If the dog is young then the dog eats the bear. If something sees the bear then it likes the dog. If something sees the dog then it is not nice. If the dog does not like the bear and the dog does not see the bear then the dog is not round. If something likes the bear and the bear does not like the dog then the bear is not round.
The bear does not like the dog.
("bear" "likes" "dog" "-")
The dog is nice.
("dog" "is" "nice" "+")
If something likes the dog then it is green.
((("something" "likes" "dog" "+")) -> ("something" "is" "green" "+"))
If something is cold and it eats the bear then the bear sees the dog.
((("something" "is" "cold" "+") ("something" "eats" "bear" "+")) -> ("bear" "sees" "dog" "+"))
If something is nice then it sees the bear.
((("something" "is" "nice" "+")) -> ("something" "sees" "bear" "+"))
If the dog is young then the dog eats the bear.
((("dog" "is" "young" "+")) -> ("dog" "eats" "bear" "+"))
If something sees the bear then it likes the dog.
((("something" "sees" "bear" "+")) -> ("something" "likes" "dog" "+"))
If something sees the dog then it is not nice.
((("something" "sees" "dog" "+")) -> ("something" "is" "nice" "-"))
If the dog does not like the bear and the dog does not see the bear then the dog is not round.
((("dog" "likes" "bear" "~") ("dog" "sees" "bear" "~")) -> ("dog" "is" "round" "-"))
If something likes the bear and the bear does not like the dog then the bear is not round.
((("something" "likes" "bear" "+") ("bear" "likes" "dog" "~")) -> ("bear" "is" "round" "-"))
The bear does not like the dog.
True
1
proof
[(triple1)]
("bear" "likes" "dog" "-")
triple1
The bear likes the dog.
False
1
inv-proof
[(triple1)]
("bear" "likes" "dog" "+")
triple1
The dog sees the bear.
True
2
proof
[(((triple2) -> rule3))]
("dog" "sees" "bear" "+")
((triple2) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog does not see the bear.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "sees" "bear" "-")
((triple2) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog likes the dog.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("dog" "likes" "dog" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2
The dog does not like the dog.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("dog" "likes" "dog" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2
The dog is green.
True
4
proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule1))]
("dog" "is" "green" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog sees the bear.
("dog" "sees" "bear" "+")
int3
The dog is not green.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule1))]
("dog" "is" "green" "-")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog sees the bear.
("dog" "sees" "bear" "+")
int3
The dog does not eat the bear.
Unknown
inv-rconc
[@1: The dog eats the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "bear" "-")
The bear sees the dog.
Unknown
rconc
[@1: The bear sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "dog" "+")
The bear is not green.
Unknown
inv-rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "green" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "bear" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The dog likes the bear.
Unknown
random
[@0: The dog likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear does not like the dog.[(triple1)] The dog is nice.[(triple2)] @1: The dog sees the bear.[(((triple2) -> rule3))] @2: The dog likes the dog.[(((((triple2) -> rule3)) -> rule5))] @3: The dog is green.[(((((((triple2) -> rule3)) -> rule5)) -> rule1))]
The bear does not like the dog.
("bear" "likes" "dog" "-")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
The dog sees the bear.
("dog" "sees" "bear" "+")
((triple2) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2
The dog is green.
("dog" "is" "green" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog sees the bear.
("dog" "sees" "bear" "+")
int3