The bear sees the dog. The dog is big. If the bear visits the dog then the dog is not blue. Cold people are nice. If someone is young and they see the bear then they are not cold. If someone sees the dog then the dog does not see the bear. If the dog does not see the bear then the dog does not like the bear. If the dog is young and the dog likes the bear then the bear does not like the dog.
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
If the bear visits the dog then the dog is not blue.
((("bear" "visits" "dog" "+")) -> ("dog" "is" "blue" "-"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is young and they see the bear then they are not cold.
((("someone" "is" "young" "+") ("someone" "sees" "bear" "+")) -> ("someone" "is" "cold" "-"))
If someone sees the dog then the dog does not see the bear.
((("someone" "sees" "dog" "+")) -> ("dog" "sees" "bear" "-"))
If the dog does not see the bear then the dog does not like the bear.
((("dog" "sees" "bear" "~")) -> ("dog" "likes" "bear" "-"))
If the dog is young and the dog likes the bear then the bear does not like the dog.
((("dog" "is" "young" "+") ("dog" "likes" "bear" "+")) -> ("bear" "likes" "dog" "-"))
The bear sees the dog.
True
1
proof
[(triple1)]
("bear" "sees" "dog" "+")
triple1
The bear does not see the dog.
False
1
inv-proof
[(triple1)]
("bear" "sees" "dog" "-")
triple1
The dog does not see the bear.
True
2
proof
[(((triple1) -> rule4))]
("dog" "sees" "bear" "-")
((triple1) -> (rule4 % int1))
The dog does not see the bear.
("dog" "sees" "bear" "-")
int1
The dog sees the bear.
False
2
inv-proof
[(((triple1) -> rule4))]
("dog" "sees" "bear" "+")
((triple1) -> (rule4 % int1))
The dog does not see the bear.
("dog" "sees" "bear" "-")
int1
The dog does not like the bear.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("dog" "likes" "bear" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog does not like the bear.
("dog" "likes" "bear" "-")
int1
The dog does not see the bear.
("dog" "sees" "bear" "-")
int2
The dog likes the bear.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("dog" "likes" "bear" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog does not like the bear.
("dog" "likes" "bear" "-")
int1
The dog does not see the bear.
("dog" "sees" "bear" "-")
int2
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "nice" "-")
The bear is nice.
Unknown
rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "nice" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The dog does not visit the bear.
Unknown
inv-random
[@0: The dog visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bear" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
@0: The bear sees the dog.[(triple1)] The dog is big.[(triple2)] @1: The dog does not see the bear.[(((triple1) -> rule4))] @2: The dog does not like the bear.[(((((triple1) -> rule4)) -> rule5))]
The bear sees the dog.
("bear" "sees" "dog" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog does not see the bear.
("dog" "sees" "bear" "-")
((triple1) -> (rule4 % int1))
The dog does not see the bear.
("dog" "sees" "bear" "-")
int1
The dog does not like the bear.
("dog" "likes" "bear" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog does not like the bear.
("dog" "likes" "bear" "-")
int1
The dog does not see the bear.
("dog" "sees" "bear" "-")
int2