The bear is red. The cat chases the mouse. The cow sees the bear. The mouse is red. If something chases the bear and the bear chases the mouse then the bear sees the cow.
The bear is red.
("bear" "is" "red" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The mouse is red.
("mouse" "is" "red" "+")
If something chases the bear and the bear chases the mouse then the bear sees the cow.
((("something" "chases" "bear" "+") ("bear" "chases" "mouse" "+")) -> ("bear" "sees" "cow" "+"))
The cat chases the mouse.
True
1
proof
[(triple2)]
("cat" "chases" "mouse" "+")
triple2
The cow does not see the bear.
False
1
inv-proof
[(triple3)]
("cow" "sees" "bear" "-")
triple3
The bear does not see the cow.
Unknown
inv-rconc
[@1: The bear sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "cow" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
@0: The bear is red.[(triple1)] The cat chases the mouse.[(triple2)] The cow sees the bear.[(triple3)] The mouse is red.[(triple4)]
The bear is red.
("bear" "is" "red" "+")
triple1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple2
The cow sees the bear.
("cow" "sees" "bear" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4