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