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