The bear chases the lion. The bear is green. The bear is nice. The bear is red. The bear is not round. The bear needs the lion. The bear visits the lion. The lion chases the bear. The lion is nice. The lion needs the bear. If someone visits the lion and the lion is red then the lion is green. If the lion is young then the lion needs the bear. If the lion needs the bear then the lion visits the bear.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is not round.
("bear" "is" "round" "-")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
If someone visits the lion and the lion is red then the lion is green.
((("someone" "visits" "lion" "+") ("lion" "is" "red" "+")) -> ("lion" "is" "green" "+"))
If the lion is young then the lion needs the bear.
((("lion" "is" "young" "+")) -> ("lion" "needs" "bear" "+"))
If the lion needs the bear then the lion visits the bear.
((("lion" "needs" "bear" "+")) -> ("lion" "visits" "bear" "+"))
The lion is nice.
True
1
proof
[(triple9)]
("lion" "is" "nice" "+")
triple9
The lion does not need the bear.
False
1
inv-proof
[(triple10)]
("lion" "needs" "bear" "-")
triple10
The lion visits the bear.
True
2
proof
[(((triple10) -> rule3))]
("lion" "visits" "bear" "+")
((triple10) -> (rule3 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion does not visit the bear.
False
2
inv-proof
[(((triple10) -> rule3))]
("lion" "visits" "bear" "-")
((triple10) -> (rule3 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "green" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The bear chases the lion.[(triple1)] The bear is green.[(triple2)] The bear is nice.[(triple3)] The bear is not round.[(triple5)] The bear is red.[(triple4)] The bear needs the lion.[(triple6)] The bear visits the lion.[(triple7)] The lion chases the bear.[(triple8)] The lion is nice.[(triple9)] The lion needs the bear.[(triple10)] @1: The lion visits the bear.[(((triple10) -> rule3))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear is not round.
("bear" "is" "round" "-")
triple5
The bear is red.
("bear" "is" "red" "+")
triple4
The bear needs the lion.
("bear" "needs" "lion" "+")
triple6
The bear visits the lion.
("bear" "visits" "lion" "+")
triple7
The lion chases the bear.
("lion" "chases" "bear" "+")
triple8
The lion is nice.
("lion" "is" "nice" "+")
triple9
The lion needs the bear.
("lion" "needs" "bear" "+")
triple10
The lion visits the bear.
("lion" "visits" "bear" "+")
((triple10) -> (rule3 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1