The bear does not visit the dog. The dog visits the mouse. The lion is rough. The mouse sees the bear. If something needs the bear and it is not red then it visits the bear.
The bear does not visit the dog.
("bear" "visits" "dog" "-")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If something needs the bear and it is not red then it visits the bear.
((("something" "needs" "bear" "+") ("something" "is" "red" "~")) -> ("something" "visits" "bear" "+"))
The lion is rough.
True
1
proof
[(triple3)]
("lion" "is" "rough" "+")
triple3
The bear visits the dog.
False
1
inv-proof
[(triple1)]
("bear" "visits" "dog" "+")
triple1
The lion does not visit the bear.
Unknown
inv-rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "bear" "-")
The dog needs the lion.
Unknown
random
[@0: The dog needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "lion" "+")
@0: The bear does not visit the dog.[(triple1)] The dog visits the mouse.[(triple2)] The lion is rough.[(triple3)] The mouse sees the bear.[(triple4)]
The bear does not visit the dog.
("bear" "visits" "dog" "-")
triple1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple4