The bear is kind. The tiger needs the bear. If the bear eats the tiger then the tiger is kind. If someone needs the tiger then the tiger likes the bear. If the bear is kind and the bear eats the tiger then the tiger does not like the bear. If someone is kind then they are not green. If someone likes the bear then they like the tiger. If someone needs the bear then the bear eats the tiger. If someone is green and they do not like the bear then the bear does not like the tiger. If someone is cold and they do not like the tiger then the tiger does not eat the bear.
The bear is kind.
("bear" "is" "kind" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If the bear eats the tiger then the tiger is kind.
((("bear" "eats" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone needs the tiger then the tiger likes the bear.
((("someone" "needs" "tiger" "+")) -> ("tiger" "likes" "bear" "+"))
If the bear is kind and the bear eats the tiger then the tiger does not like the bear.
((("bear" "is" "kind" "+") ("bear" "eats" "tiger" "+")) -> ("tiger" "likes" "bear" "-"))
If someone is kind then they are not green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "-"))
If someone likes the bear then they like the tiger.
((("someone" "likes" "bear" "+")) -> ("someone" "likes" "tiger" "+"))
If someone needs the bear then the bear eats the tiger.
((("someone" "needs" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
If someone is green and they do not like the bear then the bear does not like the tiger.
((("someone" "is" "green" "+") ("someone" "likes" "bear" "~")) -> ("bear" "likes" "tiger" "-"))
If someone is cold and they do not like the tiger then the tiger does not eat the bear.
((("someone" "is" "cold" "+") ("someone" "likes" "tiger" "~")) -> ("tiger" "eats" "bear" "-"))
The bear is kind.
True
1
proof
[(triple1)]
("bear" "is" "kind" "+")
triple1
The tiger does not need the bear.
False
1
inv-proof
[(triple2)]
("tiger" "needs" "bear" "-")
triple2
The bear eats the tiger.
True
2
proof
[(((triple2) -> rule6))]
("bear" "eats" "tiger" "+")
((triple2) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is green.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "is" "green" "+")
((triple1) -> (rule4 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The tiger is kind.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("tiger" "is" "kind" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The tiger likes the bear.
False
4
inv-proof
[(((triple1 ((triple2) -> rule6)) -> rule3))]
("tiger" "likes" "bear" "+")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The tiger does not like the bear.
("tiger" "likes" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The tiger is not green.
True
4
proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule4))]
("tiger" "is" "green" "-")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3
The tiger is green.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule4))]
("tiger" "is" "green" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3
The bear does not like the tiger.
Unknown
inv-rconc
[@1: The bear likes the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "tiger" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The bear needs the tiger.
Unknown
random
[@0: The bear needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "tiger" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is kind.[(triple1)] The tiger needs the bear.[(triple2)] @1: The bear eats the tiger.[(((triple2) -> rule6))] The bear is not green.[(((triple1) -> rule4))] @2: The tiger does not like the bear.[(((triple1 ((triple2) -> rule6)) -> rule3))] The tiger is kind.[(((((triple2) -> rule6)) -> rule1))] @3: The tiger is not green.[(((((((triple2) -> rule6)) -> rule1)) -> rule4))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((triple2) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is not green.
("bear" "is" "green" "-")
((triple1) -> (rule4 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The tiger does not like the bear.
("tiger" "likes" "bear" "-")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The tiger does not like the bear.
("tiger" "likes" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The tiger is not green.
("tiger" "is" "green" "-")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3