The example in file Ex12.4-1.key can be proved automatically using the
rule set intRule:javaSemantics (see Options -> Taclet options defaults -> intRules)
but cannot be derived using the rule set intRules:arithmeticSemanticsCheckingOF.
In contrast, the example in file Ex12.4-2.key can be proved with both rule sets.
Similar, the example in file Sect12.2.1.key can be proved using both rule sets.