The bear is green. The dog sees the bear. The tiger chases the bear. If something chases the bear and it sees the tiger then the tiger chases the dog. If something needs the dog and it chases the tiger then the dog sees the tiger. If the tiger is cold and the tiger needs the bear then the bear needs the tiger.
The bear is green.
("bear" "is" "green" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If something chases the bear and it sees the tiger then the tiger chases the dog.
((("something" "chases" "bear" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
If something needs the dog and it chases the tiger then the dog sees the tiger.
((("something" "needs" "dog" "+") ("something" "chases" "tiger" "+")) -> ("dog" "sees" "tiger" "+"))
If the tiger is cold and the tiger needs the bear then the bear needs the tiger.
((("tiger" "is" "cold" "+") ("tiger" "needs" "bear" "+")) -> ("bear" "needs" "tiger" "+"))
The dog sees the bear.
True
1
proof
[(triple2)]
("dog" "sees" "bear" "+")
triple2
The tiger does not chase the bear.
False
1
inv-proof
[(triple3)]
("tiger" "chases" "bear" "-")
triple3
The dog does not see the tiger.
Unknown
inv-rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "tiger" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The bear is green.[(triple1)] The dog sees the bear.[(triple2)] The tiger chases the bear.[(triple3)]
The bear is green.
("bear" "is" "green" "+")
triple1
The dog sees the bear.
("dog" "sees" "bear" "+")
triple2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple3