The bear sees the dog. The dog needs the bear. The mouse sees the tiger. The tiger likes the dog. If someone sees the mouse then the mouse likes the bear. If the tiger needs the bear and the tiger likes the bear then the tiger is round. If the mouse sees the tiger and the mouse needs the tiger then the mouse likes the bear.
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If someone sees the mouse then the mouse likes the bear.
((("someone" "sees" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If the tiger needs the bear and the tiger likes the bear then the tiger is round.
((("tiger" "needs" "bear" "+") ("tiger" "likes" "bear" "+")) -> ("tiger" "is" "round" "+"))
If the mouse sees the tiger and the mouse needs the tiger then the mouse likes the bear.
((("mouse" "sees" "tiger" "+") ("mouse" "needs" "tiger" "+")) -> ("mouse" "likes" "bear" "+"))
The dog needs the bear.
True
1
proof
[(triple2)]
("dog" "needs" "bear" "+")
triple2
The mouse does not see the tiger.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "tiger" "-")
triple3
The mouse does not like the bear.
Unknown
inv-rconc
[@1: The mouse likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "bear" "-")
The dog likes the tiger.
Unknown
random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "+")
@0: The bear sees the dog.[(triple1)] The dog needs the bear.[(triple2)] The mouse sees the tiger.[(triple3)] The tiger likes the dog.[(triple4)]
The bear sees the dog.
("bear" "sees" "dog" "+")
triple1
The dog needs the bear.
("dog" "needs" "bear" "+")
triple2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple3
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple4