The bear eats the lion. The bear is blue. The bear is green. The bear needs the lion. The bear sees the tiger. The lion eats the bear. The lion eats the tiger. The lion is not blue. The lion is cold. The lion needs the bear. The lion needs the tiger. The lion sees the tiger. The tiger does not eat the bear. The tiger is round. The tiger sees the bear. The tiger sees the lion. If someone sees the lion then they need the bear. If someone eats the bear then they need the bear. If someone sees the tiger then the tiger is rough. If the bear is green then the bear is cold. If someone is rough and they see the bear then they are not cold. If the tiger does not eat the lion then the tiger needs the bear. If the lion is blue then the lion sees the bear. If someone is blue and they do not need the bear then they need the lion.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is green.
("bear" "is" "green" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is not blue.
("lion" "is" "blue" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone sees the lion then they need the bear.
((("someone" "sees" "lion" "+")) -> ("someone" "needs" "bear" "+"))
If someone eats the bear then they need the bear.
((("someone" "eats" "bear" "+")) -> ("someone" "needs" "bear" "+"))
If someone sees the tiger then the tiger is rough.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If the bear is green then the bear is cold.
((("bear" "is" "green" "+")) -> ("bear" "is" "cold" "+"))
If someone is rough and they see the bear then they are not cold.
((("someone" "is" "rough" "+") ("someone" "sees" "bear" "+")) -> ("someone" "is" "cold" "-"))
If the tiger does not eat the lion then the tiger needs the bear.
((("tiger" "eats" "lion" "~")) -> ("tiger" "needs" "bear" "+"))
If the lion is blue then the lion sees the bear.
((("lion" "is" "blue" "+")) -> ("lion" "sees" "bear" "+"))
If someone is blue and they do not need the bear then they need the lion.
((("someone" "is" "blue" "+") ("someone" "needs" "bear" "~")) -> ("someone" "needs" "lion" "+"))
The lion needs the tiger.
True
1
proof
[(triple11)]
("lion" "needs" "tiger" "+")
triple11
The lion is blue.
False
1
inv-proof
[(triple8)]
("lion" "is" "blue" "+")
triple8
The tiger needs the bear.
True
2
proof
[(((triple16) -> rule1))]
("tiger" "needs" "bear" "+")
((triple16) -> (rule1 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger is not rough.
False
2
inv-proof
[(((triple12) -> rule3) OR ((triple5) -> rule3))]
("tiger" "is" "rough" "-")
((triple12) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
((triple5) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not cold.
True
4
proof
[(((((triple12) -> rule3) triple15) -> rule5) OR ((((triple5) -> rule3) triple15) -> rule5))]
("tiger" "is" "cold" "-")
((((triple12) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
((((triple5) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is cold.
False
4
inv-proof
[(((((triple12) -> rule3) triple15) -> rule5) OR ((((triple5) -> rule3) triple15) -> rule5))]
("tiger" "is" "cold" "+")
((((triple12) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
((((triple5) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "bear" "-")
The tiger needs the lion.
Unknown
rconc
[@1: The tiger needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "needs" "lion" "+")
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 tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The bear eats the lion.[(triple1)] The bear is blue.[(triple2)] The bear is green.[(triple3)] The bear needs the lion.[(triple4)] The bear sees the tiger.[(triple5)] The lion eats the bear.[(triple6)] The lion eats the tiger.[(triple7)] The lion is cold.[(triple9)] The lion is not blue.[(triple8)] The lion needs the bear.[(triple10 OR ((triple6) -> rule2))] The lion needs the tiger.[(triple11)] The lion sees the tiger.[(triple12)] The tiger does not eat the bear.[(triple13)] The tiger is round.[(triple14)] The tiger sees the bear.[(triple15)] The tiger sees the lion.[(triple16)] @1: The bear is cold.[(((triple3) -> rule4))] The tiger is rough.[(((triple12) -> rule3) OR ((triple5) -> rule3))] The tiger needs the bear.[(((triple16) -> rule1))] @2: The tiger is not cold.[(((((triple12) -> rule3) triple15) -> rule5) OR ((((triple5) -> rule3) triple15) -> rule5))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear needs the lion.
("bear" "needs" "lion" "+")
triple4
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple5
The lion eats the bear.
("lion" "eats" "bear" "+")
triple6
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
triple9
The lion is not blue.
("lion" "is" "blue" "-")
triple8
The lion needs the bear.
("lion" "needs" "bear" "+")
triple10
((triple6) -> (rule2 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple11
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple12
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple15
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple16
The bear is cold.
("bear" "is" "cold" "+")
((triple3) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple12) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
((triple5) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((triple16) -> (rule1 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger is not cold.
("tiger" "is" "cold" "-")
((((triple12) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
((((triple5) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2