====================================== B_BOXING (invariant admissibility) Successfully verified. ====================================== ANY.default_create (creator, inherited by B_BOXING) Successfully verified. ====================================== B_BOXING.boxing Verification failed. Line: 33. Check has_to_fail may be violated.