The bear is young. The bear needs the squirrel. The cat is big. The cat sees the bear. The squirrel sees the cat. The tiger is big. The tiger sees the bear. If something chases the squirrel and the squirrel needs the tiger then the tiger needs the bear.
The bear is young.
("bear" "is" "young" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The cat is big.
("cat" "is" "big" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something chases the squirrel and the squirrel needs the tiger then the tiger needs the bear.
((("something" "chases" "squirrel" "+") ("squirrel" "needs" "tiger" "+")) -> ("tiger" "needs" "bear" "+"))
The cat sees the bear.
True
1
proof
[(triple4)]
("cat" "sees" "bear" "+")
triple4
The tiger is not big.
False
1
inv-proof
[(triple6)]
("tiger" "is" "big" "-")
triple6
The tiger does not need the bear.
Unknown
inv-rconc
[@1: The tiger needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "bear" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The bear is young.[(triple1)] The bear needs the squirrel.[(triple2)] The cat is big.[(triple3)] The cat sees the bear.[(triple4)] The squirrel sees the cat.[(triple5)] The tiger is big.[(triple6)] The tiger sees the bear.[(triple7)]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat sees the bear.
("cat" "sees" "bear" "+")
triple4
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple7