The bear is round. All cold people are nice. If someone is blue and round then they are cold. If someone is round then they are cold. Round people are cold. Nice people are blue. If the bear is big then the bear is round. If the bear is nice and the bear is round then the bear is cold. If someone is cold then they are not big.
The bear is round.
("bear" "is" "round" "+")
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and round then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If the bear is big then the bear is round.
((("bear" "is" "big" "+")) -> ("bear" "is" "round" "+"))
If the bear is nice and the bear is round then the bear is cold.
((("bear" "is" "nice" "+") ("bear" "is" "round" "+")) -> ("bear" "is" "cold" "+"))
If someone is cold then they are not big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
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 cold.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("bear" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is not cold.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("bear" "is" "cold" "-")
((triple1) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule4)) -> rule1))]
("bear" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8) OR ((((triple1) -> rule4)) -> rule8))]
("bear" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The bear is not big.
("bear" "is" "big" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The bear is not big.
("bear" "is" "big" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule5) OR ((((((triple1) -> rule4)) -> rule1)) -> rule5))]
("bear" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear is not blue.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule5) OR ((((((triple1) -> rule4)) -> rule1)) -> rule5))]
("bear" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
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 bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear is round.[(triple1)] @1: The bear is cold.[(((triple1) -> rule3) OR ((triple1) -> rule4))] @2: The bear is nice.[(((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] The bear is not big.[(((((triple1) -> rule3)) -> rule8) OR ((((triple1) -> rule4)) -> rule8))] @3: The bear is blue.[(((((((triple1) -> rule3)) -> rule1)) -> rule5) OR ((((((triple1) -> rule4)) -> rule1)) -> rule5))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is not big.
("bear" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The bear is not big.
("bear" "is" "big" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The bear is not big.
("bear" "is" "big" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3