======================================
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.