The bear sees the tiger. The tiger needs the bear. If someone eats the tiger then they are red. If the bear is green then the bear needs the tiger. If someone eats the bear and they are not young then the bear needs the tiger. If someone eats the bear and they are not rough then the bear does not need the tiger. If someone is green then they eat the tiger. If someone is red then they eat the bear. If someone eats the bear then they are green. If someone sees the tiger then the tiger is red.
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If someone eats the tiger then they are red.
((("someone" "eats" "tiger" "+")) -> ("someone" "is" "red" "+"))
If the bear is green then the bear needs the tiger.
((("bear" "is" "green" "+")) -> ("bear" "needs" "tiger" "+"))
If someone eats the bear and they are not young then the bear needs the tiger.
((("someone" "eats" "bear" "+") ("someone" "is" "young" "~")) -> ("bear" "needs" "tiger" "+"))
If someone eats the bear and they are not rough then the bear does not need the tiger.
((("someone" "eats" "bear" "+") ("someone" "is" "rough" "~")) -> ("bear" "needs" "tiger" "-"))
If someone is green then they eat the tiger.
((("someone" "is" "green" "+")) -> ("someone" "eats" "tiger" "+"))
If someone is red then they eat the bear.
((("someone" "is" "red" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the bear then they are green.
((("someone" "eats" "bear" "+")) -> ("someone" "is" "green" "+"))
If someone sees the tiger then the tiger is red.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "red" "+"))
The tiger needs the bear.
True
1
proof
[(triple2)]
("tiger" "needs" "bear" "+")
triple2
The tiger does not need the bear.
False
1
inv-proof
[(triple2)]
("tiger" "needs" "bear" "-")
triple2
The tiger is red.
True
2
proof
[(((triple1) -> rule8))]
("tiger" "is" "red" "+")
((triple1) -> (rule8 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is not red.
False
2
inv-proof
[(((triple1) -> rule8))]
("tiger" "is" "red" "-")
((triple1) -> (rule8 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the bear.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("tiger" "eats" "bear" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger does not eat the bear.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule6))]
("tiger" "eats" "bear" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is green.
True
4
proof
[(((((((triple1) -> rule8)) -> rule6)) -> rule7))]
("tiger" "is" "green" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is not green.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule6)) -> rule7))]
("tiger" "is" "green" "-")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The bear does not eat the bear.
Unknown
inv-rconc
[@4: The bear eats the bear.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule5 <- rule7 <- FAIL)]]
("bear" "eats" "bear" "-")
The bear needs the tiger.
Unknown
rconc
[@5: The bear needs the tiger.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule6 <- rule1 <- rule5 <- FAIL)]]
("bear" "needs" "tiger" "+")
The bear is not red.
Unknown
inv-rconc
[@4: The bear is red.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule7 <- rule6 <- FAIL)]]
("bear" "is" "red" "-")
The bear is green.
Unknown
rconc
[@4: The bear is green.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule1 <- rule5 <- FAIL)]]
("bear" "is" "green" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The bear sees the tiger.[(triple1)] The tiger needs the bear.[(triple2)] @1: The tiger is red.[(((triple1) -> rule8))] @2: The tiger eats the bear.[(((((triple1) -> rule8)) -> rule6))] @3: The tiger is green.[(((((((triple1) -> rule8)) -> rule6)) -> rule7))] @4: The tiger eats the tiger.[(((((((((triple1) -> rule8)) -> rule6)) -> rule7)) -> rule5))]
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple2
The tiger is red.
("tiger" "is" "red" "+")
((triple1) -> (rule8 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((((((triple1) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4