The bear sees the lion. The lion sees the mouse. The mouse chases the bear. The mouse is green. The mouse is nice. The mouse is rough. The mouse visits the lion. If something visits the lion then it is nice.
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something visits the lion then it is nice.
((("something" "visits" "lion" "+")) -> ("something" "is" "nice" "+"))
The mouse chases the bear.
True
1
proof
[(triple3)]
("mouse" "chases" "bear" "+")
triple3
The mouse is not green.
False
1
inv-proof
[(triple4)]
("mouse" "is" "green" "-")
triple4
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "nice" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The bear sees the lion.[(triple1)] The lion sees the mouse.[(triple2)] The mouse chases the bear.[(triple3)] The mouse is green.[(triple4)] The mouse is nice.[(triple5 OR ((triple7) -> rule1))] The mouse is rough.[(triple6)] The mouse visits the lion.[(triple7)]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple3
The mouse is green.
("mouse" "is" "green" "+")
triple4
The mouse is nice.
("mouse" "is" "nice" "+")
triple5
((triple7) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple7