The bear is round. All round things are green. If something is green then it is cold. If something is round and green then it is cold. All green things are cold. If something is green then it is cold. If the bear is round and the bear is not green then the bear is not young. If the bear is not young then the bear is not cold. If the bear is green and the bear is cold then the bear is nice.
The bear is round.
("bear" "is" "round" "+")
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is round and green then it is cold.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If the bear is round and the bear is not green then the bear is not young.
((("bear" "is" "round" "+") ("bear" "is" "green" "~")) -> ("bear" "is" "young" "-"))
If the bear is not young then the bear is not cold.
((("bear" "is" "young" "~")) -> ("bear" "is" "cold" "-"))
If the bear is green and the bear is cold then the bear is nice.
((("bear" "is" "green" "+") ("bear" "is" "cold" "+")) -> ("bear" "is" "nice" "+"))
The bear is round.
True
1
proof
[(triple1)]
("bear" "is" "round" "+")
triple1
The bear is not round.
False
1
inv-proof
[(triple1)]
("bear" "is" "round" "-")
triple1
The bear is green.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "green" "+")
((triple1) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "green" "-")
((triple1) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule1)) -> rule5) OR ((triple1 ((triple1) -> rule1)) -> rule3))]
("bear" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule1)) -> rule5) OR ((triple1 ((triple1) -> rule1)) -> rule3))]
("bear" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is nice.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule4)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule3)) -> rule8))]
("bear" "is" "nice" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
The bear is not nice.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule4)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule3)) -> rule8))]
("bear" "is" "nice" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
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 round.[(triple1)] @1: The bear is green.[(((triple1) -> rule1))] @2: The bear is cold.[(((((triple1) -> rule1)) -> rule2) OR ((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule1)) -> rule5) OR ((triple1 ((triple1) -> rule1)) -> rule3))] @3: The bear is nice.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule4)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule3)) -> rule8))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
((triple1) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3