The bear is round. The bear needs the tiger. The bear sees the tiger. The tiger eats the bear. The tiger is big. The tiger is cold. The tiger is rough. The tiger is round. The tiger needs the bear. The tiger sees the bear. If someone is cold and they need the bear then the bear is big. If the tiger sees the bear and the bear does not see the tiger then the bear eats the tiger. All big people are not green. If someone eats the bear and they do not see the bear then they do not need the bear. If someone is rough and they see the bear then they are cold. If someone sees the bear and they eat the tiger then the tiger eats the bear.
The bear is round.
("bear" "is" "round" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If someone is cold and they need the bear then the bear is big.
((("someone" "is" "cold" "+") ("someone" "needs" "bear" "+")) -> ("bear" "is" "big" "+"))
If the tiger sees the bear and the bear does not see the tiger then the bear eats the tiger.
((("tiger" "sees" "bear" "+") ("bear" "sees" "tiger" "~")) -> ("bear" "eats" "tiger" "+"))
All big people are not green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "-"))
If someone eats the bear and they do not see the bear then they do not need the bear.
((("someone" "eats" "bear" "+") ("someone" "sees" "bear" "~")) -> ("someone" "needs" "bear" "-"))
If someone is rough and they see the bear then they are cold.
((("someone" "is" "rough" "+") ("someone" "sees" "bear" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the bear and they eat the tiger then the tiger eats the bear.
((("someone" "sees" "bear" "+") ("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "bear" "+"))
The bear is round.
True
1
proof
[(triple1)]
("bear" "is" "round" "+")
triple1
The tiger does not see the bear.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "bear" "-")
triple10
The tiger is not green.
True
2
proof
[(((triple5) -> rule3))]
("tiger" "is" "green" "-")
((triple5) -> (rule3 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger is green.
False
2
inv-proof
[(((triple5) -> rule3))]
("tiger" "is" "green" "+")
((triple5) -> (rule3 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The bear is not green.
True
4
proof
[(((((triple6 triple9) -> rule1)) -> rule3) OR ((((((triple7 triple10) -> rule5) triple9) -> rule1)) -> rule3))]
("bear" "is" "green" "-")
((((triple6 triple9) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((((triple7 triple10) -> (rule5 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The bear is green.
False
4
inv-proof
[(((((triple6 triple9) -> rule1)) -> rule3) OR ((((((triple7 triple10) -> rule5) triple9) -> rule1)) -> rule3))]
("bear" "is" "green" "+")
((((triple6 triple9) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((((triple7 triple10) -> (rule5 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The bear does not eat the tiger.
Unknown
inv-rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "tiger" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "cold" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is round.[(triple1)] The bear needs the tiger.[(triple2)] The bear sees the tiger.[(triple3)] The tiger eats the bear.[(triple4)] The tiger is big.[(triple5)] The tiger is cold.[(triple6 OR ((triple7 triple10) -> rule5))] The tiger is rough.[(triple7)] The tiger is round.[(triple8)] The tiger needs the bear.[(triple9)] The tiger sees the bear.[(triple10)] @1: The bear is big.[(((triple6 triple9) -> rule1) OR ((((triple7 triple10) -> rule5) triple9) -> rule1))] The tiger is not green.[(((triple5) -> rule3))] @2: The bear is not green.[(((((triple6 triple9) -> rule1)) -> rule3) OR ((((((triple7 triple10) -> rule5) triple9) -> rule1)) -> rule3))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple3
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
((triple7 triple10) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The tiger is round.
("tiger" "is" "round" "+")
triple8
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple9
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple10
The bear is big.
("bear" "is" "big" "+")
((triple6 triple9) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
((((triple7 triple10) -> (rule5 % int2)) triple9) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is not green.
("tiger" "is" "green" "-")
((triple5) -> (rule3 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The bear is not green.
("bear" "is" "green" "-")
((((triple6 triple9) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((((triple7 triple10) -> (rule5 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3