The bear visits the tiger. The cow visits the bear. The tiger chases the bear. If the cow visits the bear and the cow chases the tiger then the bear chases the cow.
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If the cow visits the bear and the cow chases the tiger then the bear chases the cow.
((("cow" "visits" "bear" "+") ("cow" "chases" "tiger" "+")) -> ("bear" "chases" "cow" "+"))
The cow visits the bear.
True
1
proof
[(triple2)]
("cow" "visits" "bear" "+")
triple2
The bear does not visit the tiger.
False
1
inv-proof
[(triple1)]
("bear" "visits" "tiger" "-")
triple1
The bear does not chase the cow.
Unknown
inv-rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "cow" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear visits the tiger.[(triple1)] The cow visits the bear.[(triple2)] The tiger chases the bear.[(triple3)]
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple1
The cow visits the bear.
("cow" "visits" "bear" "+")
triple2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple3