The bear needs the tiger. The squirrel chases the tiger. The tiger sees the squirrel. If something sees the tiger and the tiger does not need the squirrel then the squirrel needs the tiger. If something sees the tiger and it is not young then the tiger is cold. If something sees the tiger then it chases the tiger. If something needs the squirrel then it does not chase the squirrel. If something needs the tiger then it does not see the tiger. If something is cold and it chases the tiger then the tiger is red.
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something sees the tiger and the tiger does not need the squirrel then the squirrel needs the tiger.
((("something" "sees" "tiger" "+") ("tiger" "needs" "squirrel" "~")) -> ("squirrel" "needs" "tiger" "+"))
If something sees the tiger and it is not young then the tiger is cold.
((("something" "sees" "tiger" "+") ("something" "is" "young" "~")) -> ("tiger" "is" "cold" "+"))
If something sees the tiger then it chases the tiger.
((("something" "sees" "tiger" "+")) -> ("something" "chases" "tiger" "+"))
If something needs the squirrel then it does not chase the squirrel.
((("something" "needs" "squirrel" "+")) -> ("something" "chases" "squirrel" "-"))
If something needs the tiger then it does not see the tiger.
((("something" "needs" "tiger" "+")) -> ("something" "sees" "tiger" "-"))
If something is cold and it chases the tiger then the tiger is red.
((("something" "is" "cold" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "is" "red" "+"))
The tiger sees the squirrel.
True
1
proof
[(triple3)]
("tiger" "sees" "squirrel" "+")
triple3
The tiger does not see the squirrel.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "squirrel" "-")
triple3
The squirrel does not need the tiger.
Unknown
inv-rconc
[@1: The squirrel needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "tiger" "-")
The squirrel sees the tiger.
Unknown
random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "+")
@0: The bear needs the tiger.[(triple1)] The squirrel chases the tiger.[(triple2)] The tiger sees the squirrel.[(triple3)] @1: The bear does not see the tiger.[(((triple1) -> rule5))]
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple3
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
((triple1) -> (rule5 % int1))
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int1