The bald eagle needs the tiger. The bear needs the bald eagle. The mouse chases the bear. The tiger sees the bald eagle. If something needs the tiger and the tiger is round then the tiger is green. If something chases the bald eagle then it sees the bald eagle. If something needs the bald eagle then it needs the tiger.
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
If something needs the tiger and the tiger is round then the tiger is green.
((("something" "needs" "tiger" "+") ("tiger" "is" "round" "+")) -> ("tiger" "is" "green" "+"))
If something chases the bald eagle then it sees the bald eagle.
((("something" "chases" "bald eagle" "+")) -> ("something" "sees" "bald eagle" "+"))
If something needs the bald eagle then it needs the tiger.
((("something" "needs" "bald eagle" "+")) -> ("something" "needs" "tiger" "+"))
The tiger sees the bald eagle.
True
1
proof
[(triple4)]
("tiger" "sees" "bald eagle" "+")
triple4
The tiger does not see the bald eagle.
False
1
inv-proof
[(triple4)]
("tiger" "sees" "bald eagle" "-")
triple4
The tiger is not green.
Unknown
inv-rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "green" "-")
The bald eagle sees the tiger.
Unknown
random
[@0: The bald eagle sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "tiger" "+")
@0: The bald eagle needs the tiger.[(triple1)] The bear needs the bald eagle.[(triple2)] The mouse chases the bear.[(triple3)] The tiger sees the bald eagle.[(triple4)] @1: The bear needs the tiger.[(((triple2) -> rule3))]
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
triple1
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
triple2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple3
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
triple4
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple2) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1