The bear is round. Round things are big. If the bear is big then the bear is rough. If something is rough then it is not red.
The bear is round.
("bear" "is" "round" "+")
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If the bear is big then the bear is rough.
((("bear" "is" "big" "+")) -> ("bear" "is" "rough" "+"))
If something is rough then it is not red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "-"))
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 big.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "big" "+")
((triple1) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "big" "-")
((triple1) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("bear" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is not rough.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("bear" "is" "rough" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is not red.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("bear" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear is not red.
("bear" "is" "red" "-")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The bear is red.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("bear" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear is not red.
("bear" "is" "red" "-")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is big.
("bear" "is" "big" "+")
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 needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear is round.[(triple1)] @1: The bear is big.[(((triple1) -> rule1))] @2: The bear is rough.[(((((triple1) -> rule1)) -> rule2))] @3: The bear is not red.[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
((triple1) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is not red.
("bear" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear is not red.
("bear" "is" "red" "-")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3