The bear chases the rabbit. The bear is blue. The bear is green. The lion chases the bear. The lion is blue. The lion is nice. The lion needs the bear. The lion needs the rabbit. The rabbit is blue. The rabbit needs the bear. The rabbit needs the lion. The rabbit sees the bear. If something is nice and blue then it needs the bear. If something chases the bear then the bear sees the lion.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is green.
("bear" "is" "green" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
If something is nice and blue then it needs the bear.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "bear" "+"))
If something chases the bear then the bear sees the lion.
((("something" "chases" "bear" "+")) -> ("bear" "sees" "lion" "+"))
The lion chases the bear.
True
1
proof
[(triple4)]
("lion" "chases" "bear" "+")
triple4
The lion is not nice.
False
1
inv-proof
[(triple6)]
("lion" "is" "nice" "-")
triple6
The bear sees the lion.
True
2
proof
[(((triple4) -> rule2))]
("bear" "sees" "lion" "+")
((triple4) -> (rule2 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear does not see the lion.
False
2
inv-proof
[(((triple4) -> rule2))]
("bear" "sees" "lion" "-")
((triple4) -> (rule2 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "bear" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The lion does not see the rabbit.
Unknown
inv-random
[@0: The lion sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The bear chases the rabbit.[(triple1)] The bear is blue.[(triple2)] The bear is green.[(triple3)] The lion chases the bear.[(triple4)] The lion is blue.[(triple5)] The lion is nice.[(triple6)] The lion needs the bear.[(triple7 OR ((triple6 triple5) -> rule1))] The lion needs the rabbit.[(triple8)] The rabbit is blue.[(triple9)] The rabbit needs the bear.[(triple10)] The rabbit needs the lion.[(triple11)] The rabbit sees the bear.[(triple12)] @1: The bear sees the lion.[(((triple4) -> rule2))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The lion chases the bear.
("lion" "chases" "bear" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is nice.
("lion" "is" "nice" "+")
triple6
The lion needs the bear.
("lion" "needs" "bear" "+")
triple7
((triple6 triple5) -> (rule1 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple10
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple11
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple12
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple4) -> (rule2 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1