The bear is red. The lion needs the tiger. The tiger needs the bear. If someone is young and they eat the lion then the lion needs the bear. If someone sees the bear and the bear is young then they see the tiger. If someone needs the tiger then they are blue. If the tiger sees the bear and the bear is red then the bear eats the lion. All nice, blue people are red. If someone is blue then they eat the lion. Red people are young. If someone eats the bear and they need the bear then the bear needs the lion.
The bear is red.
("bear" "is" "red" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If someone is young and they eat the lion then the lion needs the bear.
((("someone" "is" "young" "+") ("someone" "eats" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If someone sees the bear and the bear is young then they see the tiger.
((("someone" "sees" "bear" "+") ("bear" "is" "young" "+")) -> ("someone" "sees" "tiger" "+"))
If someone needs the tiger then they are blue.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "blue" "+"))
If the tiger sees the bear and the bear is red then the bear eats the lion.
((("tiger" "sees" "bear" "+") ("bear" "is" "red" "+")) -> ("bear" "eats" "lion" "+"))
All nice, blue people are red.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is blue then they eat the lion.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "lion" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone eats the bear and they need the bear then the bear needs the lion.
((("someone" "eats" "bear" "+") ("someone" "needs" "bear" "+")) -> ("bear" "needs" "lion" "+"))
The bear is red.
True
1
proof
[(triple1)]
("bear" "is" "red" "+")
triple1
The bear is not red.
False
1
inv-proof
[(triple1)]
("bear" "is" "red" "-")
triple1
The lion is blue.
True
2
proof
[(((triple2) -> rule3))]
("lion" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple1) -> rule7))]
("bear" "is" "young" "-")
((triple1) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The lion does not need the bear.
Unknown
inv-rconc
[@3: The lion needs the bear.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule5 <- FAIL)]]
("lion" "needs" "bear" "-")
The lion sees the tiger.
Unknown
rconc
[@1: The lion sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "tiger" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The bear needs the tiger.
Unknown
random
[@0: The bear needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "tiger" "+")
@0: The bear is red.[(triple1)] The lion needs the tiger.[(triple2)] The tiger needs the bear.[(triple3)] @1: The bear is young.[(((triple1) -> rule7))] The lion is blue.[(((triple2) -> rule3))] @2: The lion eats the lion.[(((((triple2) -> rule3)) -> rule6))]
The bear is red.
("bear" "is" "red" "+")
triple1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2