The bear is red. The dog visits the bear. If the bear is rough then the bear does not chase the dog. If something visits the bear then the bear chases the dog. All young things are not big. If something eats the bear then the bear eats the dog. If something eats the bear and it is not rough then it is kind. If something is big and not rough then it chases the dog. If the dog visits the bear and the bear does not visit the dog then the dog does not chase the bear. If something visits the dog and it is not big then it chases the bear.
The bear is red.
("bear" "is" "red" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
If the bear is rough then the bear does not chase the dog.
((("bear" "is" "rough" "+")) -> ("bear" "chases" "dog" "-"))
If something visits the bear then the bear chases the dog.
((("something" "visits" "bear" "+")) -> ("bear" "chases" "dog" "+"))
All young things are not big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "-"))
If something eats the bear then the bear eats the dog.
((("something" "eats" "bear" "+")) -> ("bear" "eats" "dog" "+"))
If something eats the bear and it is not rough then it is kind.
((("something" "eats" "bear" "+") ("something" "is" "rough" "~")) -> ("something" "is" "kind" "+"))
If something is big and not rough then it chases the dog.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "chases" "dog" "+"))
If the dog visits the bear and the bear does not visit the dog then the dog does not chase the bear.
((("dog" "visits" "bear" "+") ("bear" "visits" "dog" "~")) -> ("dog" "chases" "bear" "-"))
If something visits the dog and it is not big then it chases the bear.
((("something" "visits" "dog" "+") ("something" "is" "big" "~")) -> ("something" "chases" "bear" "+"))
The bear is red.
True
1
proof
[(triple1)]
("bear" "is" "red" "+")
triple1
The bear is not red.
False
1
inv-proof
[(triple1)]
("bear" "is" "red" "-")
triple1
The bear chases the dog.
True
2
proof
[(((triple2) -> rule2))]
("bear" "chases" "dog" "+")
((triple2) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The bear does not chase the dog.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "chases" "dog" "-")
((triple2) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "chases" "bear" "-")
The dog chases the bear.
Unknown
rconc
[@1: The dog chases the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "chases" "bear" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear is red.[(triple1)] The dog visits the bear.[(triple2)] @1: The bear chases the dog.[(((triple2) -> rule2))]
The bear is red.
("bear" "is" "red" "+")
triple1
The dog visits the bear.
("dog" "visits" "bear" "+")
triple2
The bear chases the dog.
("bear" "chases" "dog" "+")
((triple2) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1