The bear is not green. The bear is nice. The bear sees the lion. The lion is not nice. The lion needs the bear. The lion sees the bear. The lion visits the bear. If the bear visits the lion and the bear is not blue then the bear is young. If the bear needs the lion and the lion is blue then the bear is big. If the bear visits the lion then the lion is nice. If something visits the lion and the lion visits the bear then the lion is nice. If something is young and not blue then it is big. If something is nice then it needs the bear. If the bear sees the lion and the bear is green then the lion sees the bear. If the bear needs the lion and the lion visits the bear then the bear sees the lion.
The bear is not green.
("bear" "is" "green" "-")
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If the bear visits the lion and the bear is not blue then the bear is young.
((("bear" "visits" "lion" "+") ("bear" "is" "blue" "~")) -> ("bear" "is" "young" "+"))
If the bear needs the lion and the lion is blue then the bear is big.
((("bear" "needs" "lion" "+") ("lion" "is" "blue" "+")) -> ("bear" "is" "big" "+"))
If the bear visits the lion then the lion is nice.
((("bear" "visits" "lion" "+")) -> ("lion" "is" "nice" "+"))
If something visits the lion and the lion visits the bear then the lion is nice.
((("something" "visits" "lion" "+") ("lion" "visits" "bear" "+")) -> ("lion" "is" "nice" "+"))
If something is young and not blue then it is big.
((("something" "is" "young" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "+"))
If something is nice then it needs the bear.
((("something" "is" "nice" "+")) -> ("something" "needs" "bear" "+"))
If the bear sees the lion and the bear is green then the lion sees the bear.
((("bear" "sees" "lion" "+") ("bear" "is" "green" "+")) -> ("lion" "sees" "bear" "+"))
If the bear needs the lion and the lion visits the bear then the bear sees the lion.
((("bear" "needs" "lion" "+") ("lion" "visits" "bear" "+")) -> ("bear" "sees" "lion" "+"))
The lion sees the bear.
True
1
proof
[(triple6)]
("lion" "sees" "bear" "+")
triple6
The lion does not see the bear.
False
1
inv-proof
[(triple6)]
("lion" "sees" "bear" "-")
triple6
The bear needs the bear.
True
2
proof
[(((triple2) -> rule6))]
("bear" "needs" "bear" "+")
((triple2) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple2) -> rule6))]
("bear" "needs" "bear" "-")
((triple2) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "big" "-")
The bear is big.
Unknown
rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "big" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The bear needs the lion.
Unknown
random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "+")
@0: The bear is nice.[(triple2)] The bear is not green.[(triple1)] The bear sees the lion.[(triple3)] The lion is not nice.[(triple4)] The lion needs the bear.[(triple5)] The lion sees the bear.[(triple6)] The lion visits the bear.[(triple7)] @1: The bear needs the bear.[(((triple2) -> rule6))]
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear is not green.
("bear" "is" "green" "-")
triple1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple3
The lion is not nice.
("lion" "is" "nice" "-")
triple4
The lion needs the bear.
("lion" "needs" "bear" "+")
triple5
The lion sees the bear.
("lion" "sees" "bear" "+")
triple6
The lion visits the bear.
("lion" "visits" "bear" "+")
triple7
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple2) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1