The bald eagle chases the bear. The bald eagle sees the lion. The bear sees the bald eagle. The bear sees the tiger. The bear visits the lion. The lion chases the bald eagle. The lion is big. The lion sees the bear. The lion visits the bald eagle. The tiger chases the bald eagle. The tiger is big. The tiger is blue. The tiger is green. The tiger sees the bald eagle. The tiger visits the bear. If someone sees the tiger then they see the lion.
The bald eagle chases the bear.
("bald eagle" "chases" "bear" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
The lion is big.
("lion" "is" "big" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion visits the bald eagle.
("lion" "visits" "bald eagle" "+")
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone sees the tiger then they see the lion.
((("someone" "sees" "tiger" "+")) -> ("someone" "sees" "lion" "+"))
The lion is big.
True
1
proof
[(triple7)]
("lion" "is" "big" "+")
triple7
The tiger is not green.
False
1
inv-proof
[(triple13)]
("tiger" "is" "green" "-")
triple13
The bear sees the lion.
True
2
proof
[(((triple4) -> rule1))]
("bear" "sees" "lion" "+")
((triple4) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear does not see the lion.
False
2
inv-proof
[(((triple4) -> rule1))]
("bear" "sees" "lion" "-")
((triple4) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The tiger does not see the lion.
Unknown
inv-rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "lion" "+")
The bear does not visit the tiger.
Unknown
inv-random
[@0: The bear visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "tiger" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The bald eagle chases the bear.[(triple1)] The bald eagle sees the lion.[(triple2)] The bear sees the bald eagle.[(triple3)] The bear sees the tiger.[(triple4)] The bear visits the lion.[(triple5)] The lion chases the bald eagle.[(triple6)] The lion is big.[(triple7)] The lion sees the bear.[(triple8)] The lion visits the bald eagle.[(triple9)] The tiger chases the bald eagle.[(triple10)] The tiger is big.[(triple11)] The tiger is blue.[(triple12)] The tiger is green.[(triple13)] The tiger sees the bald eagle.[(triple14)] The tiger visits the bear.[(triple15)] @1: The bear sees the lion.[(((triple4) -> rule1))]
The bald eagle chases the bear.
("bald eagle" "chases" "bear" "+")
triple1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple2
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
triple3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple4
The bear visits the lion.
("bear" "visits" "lion" "+")
triple5
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
triple6
The lion is big.
("lion" "is" "big" "+")
triple7
The lion sees the bear.
("lion" "sees" "bear" "+")
triple8
The lion visits the bald eagle.
("lion" "visits" "bald eagle" "+")
triple9
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
triple13
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
triple14
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple4) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1