The bear eats the lion. The bear is blue. The bear is nice. The bear needs the tiger. The bear sees the lion. The lion is blue. The lion is cold. The lion is green. The lion sees the bear. The tiger eats the bear. The tiger is cold. The tiger needs the lion. If someone eats the bear then the bear is green. If someone sees the tiger and they are nice then they eat the bear. If someone is blue and cold then they need the tiger. If someone is cold then they see the bear. If someone is nice then they eat the lion. If someone is red and they see the tiger then they need the tiger.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If someone eats the bear then the bear is green.
((("someone" "eats" "bear" "+")) -> ("bear" "is" "green" "+"))
If someone sees the tiger and they are nice then they eat the bear.
((("someone" "sees" "tiger" "+") ("someone" "is" "nice" "+")) -> ("someone" "eats" "bear" "+"))
If someone is blue and cold then they need the tiger.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "needs" "tiger" "+"))
If someone is cold then they see the bear.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "bear" "+"))
If someone is nice then they eat the lion.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "lion" "+"))
If someone is red and they see the tiger then they need the tiger.
((("someone" "is" "red" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
The bear sees the lion.
True
1
proof
[(triple5)]
("bear" "sees" "lion" "+")
triple5
The lion is not green.
False
1
inv-proof
[(triple8)]
("lion" "is" "green" "-")
triple8
The tiger does not eat the lion.
Unknown
inv-rconc
[@1: The tiger eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "lion" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The bear eats the lion.[(triple1 OR ((triple3) -> rule5))] The bear is blue.[(triple2)] The bear is nice.[(triple3)] The bear needs the tiger.[(triple4)] The bear sees the lion.[(triple5)] The lion is blue.[(triple6)] The lion is cold.[(triple7)] The lion is green.[(triple8)] The lion sees the bear.[(triple9 OR ((triple7) -> rule4))] The tiger eats the bear.[(triple10)] The tiger is cold.[(triple11)] The tiger needs the lion.[(triple12)] @1: The bear is green.[(((triple10) -> rule1))] The lion needs the tiger.[(((triple6 triple7) -> rule3))] The tiger sees the bear.[(((triple11) -> rule4))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
((triple3) -> (rule5 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple4
The bear sees the lion.
("bear" "sees" "lion" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple6
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
triple8
The lion sees the bear.
("lion" "sees" "bear" "+")
triple9
((triple7) -> (rule4 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple12
The bear is green.
("bear" "is" "green" "+")
((triple10) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
((triple6 triple7) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
((triple11) -> (rule4 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1