Proof summary for theory exprd exprd_TCC1.................................proved - complete [O]( 0.24 s) exprd_TCC2.................................proved - complete [O]( 0.23 s) exprd_TCC3.................................proved - complete [O]( 0.25 s) exprd_TCC4.................................proved - complete [O]( 0.27 s) exprd_TCC5.................................proved - complete [O]( 0.29 s) exprd_TCC6.................................proved - complete [O]( 0.29 s) exprd_sign_TCC1............................proved - complete [O]( 0.22 s) exprd_sign.................................proved - complete [O]( 0.80 s) exprd_sgl_TCC1.............................proved - complete [O]( 0.23 s) exprd_sgl_TCC2.............................proved - complete [O]( 0.23 s) exprd_sgl_TCC3.............................proved - complete [O]( 0.23 s) exprd_sgl_TCC4.............................proved - complete [O]( 0.23 s) exprd_sgl_TCC5.............................proved - complete [O]( 0.23 s) exprd_sgl_TCC6.............................proved - complete [O]( 0.23 s) exprd_sgl_TCC7.............................proved - complete [O]( 1.06 s) exprd_sgl..................................proved - complete [O](42.23 s) exprd_dbl_TCC1.............................proved - complete [O]( 0.23 s) exprd_dbl_TCC2.............................proved - complete [O]( 0.23 s) exprd_dbl_TCC3.............................proved - complete [O]( 0.22 s) exprd_dbl_TCC4.............................proved - complete [O]( 0.22 s) exprd_dbl_TCC5.............................proved - complete [O]( 0.22 s) exprd_dbl_TCC6.............................proved - complete [O]( 0.22 s) exprd_dbl_TCC7.............................proved - complete [O]( 0.75 s) exprd_dbl..................................proved - complete [O](14.56 s) exprd_unmasked_ovf_sgl_TCC1................proved - complete [O]( 0.22 s) exprd_unmasked_ovf_sgl_TCC2................proved - complete [O]( 0.23 s) exprd_unmasked_ovf_sgl_TCC3................proved - complete [O]( 0.23 s) exprd_unmasked_ovf_sgl_TCC4................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC5................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC6................proved - complete [O]( 0.25 s) exprd_unmasked_ovf_sgl_TCC7................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC8................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC9................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC10...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC11...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC12...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC13...............proved - complete [O]( 4.91 s) exprd_unmasked_ovf_sgl_TCC14...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC15...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_sgl_TCC16...............proved - complete [O]( 0.25 s) exprd_unmasked_ovf_sgl_TCC17...............proved - complete [O]( 4.91 s) exprd_unmasked_ovf_sgl.....................proved - complete [O]( 7.67 s) exprd_unmasked_ovf_dbl_TCC1................proved - complete [O]( 0.22 s) exprd_unmasked_ovf_dbl_TCC2................proved - complete [O]( 0.23 s) exprd_unmasked_ovf_dbl_TCC3................proved - complete [O]( 0.23 s) exprd_unmasked_ovf_dbl_TCC4................proved - complete [O]( 0.25 s) exprd_unmasked_ovf_dbl_TCC5................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC6................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC7................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC8................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC9................proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC10...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC11...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC12...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC13...............proved - complete [O]( 3.27 s) exprd_unmasked_ovf_dbl_TCC14...............proved - complete [O]( 0.25 s) exprd_unmasked_ovf_dbl_TCC15...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC16...............proved - complete [O]( 0.24 s) exprd_unmasked_ovf_dbl_TCC17...............proved - complete [O]( 3.31 s) exprd_unmasked_ovf_dbl.....................proved - complete [O]( 7.49 s) exprd_val_sgl_TCC1.........................proved - complete [O]( 0.22 s) exprd_val_sgl_TCC2.........................proved - complete [O]( 0.23 s) exprd_val_sgl_TCC3.........................proved - complete [O]( 0.23 s) exprd_val_sgl_TCC4.........................proved - complete [O]( 2.28 s) exprd_val_sgl..............................proved - complete [O](11.53 s) exprd_val_dbl_TCC1.........................proved - complete [O]( 0.23 s) exprd_val_dbl_TCC2.........................proved - complete [O]( 0.22 s) exprd_val_dbl_TCC3.........................proved - complete [O]( 0.23 s) exprd_val_dbl_TCC4.........................proved - complete [O]( 2.29 s) exprd_val_dbl..............................proved - complete [O](11.49 s) exprd_correct_sgl..........................proved - complete [O](27.82 s) exprd_correct_dbl..........................proved - complete [O](26.14 s) Theory totals: 72 formulas, 72 attempted, 72 succeeded (185.54 s) Proof summary for theory pack_stage pack_stage_TCC1............................proved - complete [O]( 0.23 s) pack_stage_TCC2............................proved - complete [O]( 0.23 s) pack_stage_TCC3............................proved - complete [O]( 0.24 s) pack_stage_TCC4............................proved - complete [O]( 0.25 s) pack_stage_TCC5............................proved - complete [O]( 0.25 s) pack_stage_TCC6............................proved - complete [O]( 0.25 s) pack_stage_TCC7............................proved - complete [O]( 0.24 s) pack_stage_TCC8............................proved - complete [O]( 0.26 s) pack_stage_TCC9............................proved - complete [O]( 0.26 s) pack_stage_passthrough.....................proved - complete [O]( 0.42 s) pack_sig_sgl_TCC1..........................proved - complete [O]( 0.23 s) pack_sig_sgl_TCC2..........................proved - complete [O]( 0.23 s) pack_sig_sgl_TCC3..........................proved - complete [O]( 0.23 s) pack_sig_sgl_TCC4..........................proved - complete [O]( 0.22 s) pack_sig_sgl_TCC5..........................proved - complete [O]( 0.23 s) pack_sig_sgl_TCC6..........................proved - complete [O]( 0.23 s) pack_sig_sgl...............................proved - complete [O]( 1.06 s) pack_sig_dbl_TCC1..........................proved - complete [O]( 0.23 s) pack_sig_dbl_TCC2..........................proved - complete [O]( 0.23 s) pack_sig_dbl_TCC3..........................proved - complete [O]( 0.23 s) pack_sig_dbl_TCC4..........................proved - complete [O]( 0.23 s) pack_sig_dbl_TCC5..........................proved - complete [O]( 0.23 s) pack_sig_dbl_TCC6..........................proved - complete [O]( 0.23 s) pack_sig_dbl...............................proved - complete [O]( 1.07 s) pack_sgl_TCC1..............................proved - complete [O]( 0.23 s) pack_sgl_TCC2..............................proved - complete [O]( 0.23 s) pack_sgl_TCC3..............................proved - complete [O]( 0.23 s) pack_sgl_TCC4..............................proved - complete [O]( 2.47 s) pack_sgl...................................proved - complete [O]( 7.77 s) pack_dbl_TCC1..............................proved - complete [O]( 0.23 s) pack_dbl_TCC2..............................proved - complete [O]( 0.23 s) pack_dbl_TCC3..............................proved - complete [O]( 0.23 s) pack_dbl_TCC4..............................proved - complete [O]( 2.02 s) pack_dbl...................................proved - complete [O]( 6.40 s) pack_correct_sgl...........................proved - complete [O](10.62 s) pack_correct_dbl...........................proved - complete [O]( 8.76 s) Theory totals: 36 formulas, 36 attempted, 36 succeeded (46.93 s) Proof summary for theory adjexp_stage adjexp_stage_passthrough...................proved - complete [O]( 0.37 s) adjexp_tiny_sgl_TCC1.......................proved - complete [O]( 0.22 s) adjexp_tiny_sgl_TCC2.......................proved - complete [O]( 0.22 s) adjexp_tiny_sgl_TCC3.......................proved - complete [O]( 0.23 s) adjexp_tiny_sgl............................proved - complete [O]( 0.30 s) adjexp_tiny_dbl_TCC1.......................proved - complete [O]( 0.22 s) adjexp_tiny_dbl_TCC2.......................proved - complete [O]( 0.23 s) adjexp_tiny_dbl_TCC3.......................proved - complete [O]( 0.23 s) adjexp_tiny_dbl............................proved - complete [O]( 0.30 s) adjexp_ovf2_sgl_TCC1.......................proved - complete [O]( 0.23 s) adjexp_ovf2_sgl_TCC2.......................proved - complete [O]( 0.23 s) adjexp_ovf2_sgl_TCC3.......................proved - complete [O]( 0.22 s) adjexp_ovf2_sgl............................proved - complete [O]( 7.27 s) adjexp_ovf2_dbl_TCC1.......................proved - complete [O]( 0.22 s) adjexp_ovf2_dbl_TCC2.......................proved - complete [O]( 0.23 s) adjexp_ovf2_dbl_TCC3.......................proved - complete [O]( 0.23 s) adjexp_ovf2_dbl............................proved - complete [O]( 6.70 s) adjexp_ovf_sgl.............................proved - complete [O]( 0.49 s) adjexp_ovf_dbl.............................proved - complete [O]( 0.49 s) adjexp_sgl_TCC1............................proved - complete [O]( 0.23 s) adjexp_sgl_TCC2............................proved - complete [O]( 0.23 s) adjexp_sgl_TCC3............................proved - complete [O]( 0.22 s) adjexp_sgl_TCC4............................proved - complete [O]( 0.22 s) adjexp_sgl_TCC5............................proved - complete [O]( 0.23 s) adjexp_sgl_TCC6............................proved - complete [O]( 0.23 s) adjexp_sgl_TCC7............................proved - complete [O]( 0.23 s) adjexp_sgl_TCC8............................proved - complete [O]( 0.28 s) adjexp_sgl_TCC9............................proved - complete [O]( 0.36 s) adjexp_sgl_TCC10...........................proved - complete [O]( 0.24 s) adjexp_sgl.................................proved - complete [O](13.62 s) adjexp_dbl_TCC1............................proved - complete [O]( 0.23 s) adjexp_dbl_TCC2............................proved - complete [O]( 0.22 s) adjexp_dbl_TCC3............................proved - complete [O]( 0.23 s) adjexp_dbl_TCC4............................proved - complete [O]( 0.23 s) adjexp_dbl.................................proved - complete [O](12.95 s) adjexp_e_sgl_TCC1..........................proved - complete [O]( 0.23 s) adjexp_e_sgl_TCC2..........................proved - complete [O]( 0.23 s) adjexp_e_sgl_TCC3..........................proved - complete [O]( 0.23 s) adjexp_e_sgl_TCC4..........................proved - complete [O]( 0.23 s) adjexp_e_sgl...............................proved - complete [O]( 4.55 s) adjexp_e_dbl...............................proved - complete [O]( 4.39 s) Theory totals: 41 formulas, 41 attempted, 41 succeeded (58.44 s) Proof summary for theory postnorm_stage postnorm_stage_passthrough.................proved - complete [O]( 0.33 s) postnorm_stage_tiny_ovf_sgl_TCC1...........proved - complete [O]( 0.23 s) postnorm_stage_tiny_ovf_sgl_TCC2...........proved - complete [O]( 0.22 s) postnorm_stage_tiny_ovf_sgl................proved - complete [O]( 0.30 s) postnorm_stage_tiny_ovf_dbl_TCC1...........proved - complete [O]( 0.22 s) postnorm_stage_tiny_ovf_dbl_TCC2...........proved - complete [O]( 0.23 s) postnorm_stage_tiny_ovf_dbl................proved - complete [O]( 0.30 s) postnorm_stage_sgl_TCC1....................proved - complete [O]( 0.22 s) postnorm_stage_sgl_TCC2....................proved - complete [O]( 0.23 s) postnorm_stage_sgl_TCC3....................proved - complete [O]( 0.22 s) postnorm_stage_sgl_TCC4....................proved - complete [O]( 0.23 s) postnorm_stage_sgl_TCC5....................proved - complete [O]( 0.23 s) postnorm_stage_sgl_TCC6....................proved - complete [O]( 0.23 s) postnorm_stage_sgl_TCC7....................proved - complete [O]( 0.23 s) postnorm_stage_sgl_TCC8....................proved - complete [O]( 0.23 s) postnorm_stage_sgl_TCC9....................proved - complete [O]( 0.23 s) postnorm_stage_sgl_TCC10...................proved - complete [O]( 0.23 s) postnorm_stage_sgl_TCC11...................proved - complete [O]( 0.24 s) postnorm_stage_sgl_TCC12...................proved - complete [O]( 0.23 s) postnorm_stage_sgl.........................proved - complete [O](11.60 s) postnorm_stage_dbl_TCC1....................proved - complete [O]( 0.23 s) postnorm_stage_dbl_TCC2....................proved - complete [O]( 0.22 s) postnorm_stage_dbl_TCC3....................proved - complete [O]( 0.23 s) postnorm_stage_dbl_TCC4....................proved - complete [O]( 0.22 s) postnorm_stage_dbl_TCC5....................proved - complete [O]( 0.23 s) postnorm_stage_dbl_TCC6....................proved - complete [O]( 0.23 s) postnorm_stage_dbl.........................proved - complete [O]( 8.12 s) Theory totals: 27 formulas, 27 attempted, 27 succeeded (25.66 s) Proof summary for theory sigrd_stage sigrd_stage_passthrough....................proved - complete [O]( 0.36 s) sigrd_stage_tiny_ovf_sgl_TCC1..............proved - complete [O]( 0.24 s) sigrd_stage_tiny_ovf_sgl_TCC2..............proved - complete [O]( 0.24 s) sigrd_stage_tiny_ovf_sgl...................proved - complete [O]( 0.30 s) sigrd_stage_tiny_ovf_dbl_TCC1..............proved - complete [O]( 0.22 s) sigrd_stage_tiny_ovf_dbl_TCC2..............proved - complete [O]( 0.22 s) sigrd_stage_tiny_ovf_dbl...................proved - complete [O]( 0.31 s) sigrd_stage_sgl_TCC1.......................proved - complete [O]( 0.25 s) sigrd_stage_sgl_TCC2.......................proved - complete [O]( 0.26 s) sigrd_stage_sgl_TCC3.......................proved - complete [O]( 0.28 s) sigrd_stage_sgl_TCC4.......................proved - complete [O]( 0.28 s) sigrd_stage_sgl_TCC5.......................proved - complete [O]( 0.28 s) sigrd_stage_sgl_TCC6.......................proved - complete [O]( 0.28 s) sigrd_stage_sgl_TCC7.......................proved - complete [O]( 0.28 s) sigrd_stage_sgl_TCC8.......................proved - complete [O]( 0.33 s) sigrd_stage_sgl_TCC9.......................proved - complete [O]( 0.32 s) sigrd_stage_sgl_TCC10......................proved - complete [O]( 0.33 s) sigrd_stage_sgl_TCC11......................proved - complete [O]( 0.33 s) sigrd_stage_sgl_TCC12......................proved - complete [O]( 0.33 s) sigrd_stage_sgl_TCC13......................proved - complete [O]( 0.39 s) sigrd_stage_sgl_TCC14......................proved - complete [O]( 0.39 s) sigrd_stage_sgl............................proved - complete [O](22.12 s) sigrd_stage_dbl_TCC1.......................proved - complete [O]( 0.26 s) sigrd_stage_dbl_TCC2.......................proved - complete [O]( 0.25 s) sigrd_stage_dbl_TCC3.......................proved - complete [O]( 0.28 s) sigrd_stage_dbl_TCC4.......................proved - complete [O]( 0.28 s) sigrd_stage_dbl_TCC5.......................proved - complete [O]( 0.28 s) sigrd_stage_dbl_TCC6.......................proved - complete [O]( 0.31 s) sigrd_stage_dbl............................proved - complete [O](17.93 s) sigrd_stage_F_low..........................proved - complete [O]( 3.01 s) sigrd_stage_inx_sgl........................proved - complete [O]( 8.64 s) sigrd_stage_inx_dbl........................proved - complete [O]( 7.21 s) Theory totals: 32 formulas, 32 attempted, 32 succeeded (66.79 s) Proof summary for theory repp_stage repp_stage_passthrough.....................proved - complete [O]( 0.29 s) repp_stage_tiny_ovf_sgl_TCC1...............proved - complete [O]( 0.22 s) repp_stage_tiny_ovf_sgl_TCC2...............proved - complete [O]( 0.22 s) repp_stage_tiny_ovf_sgl....................proved - complete [O]( 3.80 s) repp_stage_tiny_ovf_dbl_TCC1...............proved - complete [O]( 0.22 s) repp_stage_tiny_ovf_dbl_TCC2...............proved - complete [O]( 0.23 s) repp_stage_tiny_ovf_dbl....................proved - complete [O]( 3.74 s) repp_lem...................................proved - complete [O]( 0.63 s) repp_stage_sgl_TCC1........................proved - complete [O]( 0.22 s) repp_stage_sgl_TCC2........................proved - complete [O]( 0.22 s) repp_stage_sgl_TCC3........................proved - complete [O]( 0.22 s) repp_stage_sgl_TCC4........................proved - complete [O]( 0.23 s) repp_stage_sgl_TCC5........................proved - complete [O]( 0.23 s) repp_stage_sgl_TCC6........................proved - complete [O]( 0.23 s) repp_stage_sgl_TCC7........................proved - complete [O]( 0.23 s) repp_stage_sgl_TCC8........................proved - complete [O]( 0.23 s) repp_stage_sgl_TCC9........................proved - complete [O]( 0.22 s) repp_stage_sgl_TCC10.......................proved - complete [O]( 0.23 s) repp_stage_sgl_TCC11.......................proved - complete [O]( 0.31 s) repp_stage_sgl_TCC12.......................proved - complete [O]( 0.24 s) repp_stage_sgl_TCC13.......................proved - complete [O]( 0.24 s) repp_stage_sgl_TCC14.......................proved - complete [O]( 0.24 s) repp_stage_sgl_TCC15.......................proved - complete [O]( 0.42 s) repp_stage_sgl_TCC16.......................proved - complete [O]( 0.42 s) repp_stage_sgl.............................proved - complete [O](15.59 s) repp_stage_dbl_TCC1........................proved - complete [O]( 0.22 s) repp_stage_dbl_TCC2........................proved - complete [O]( 0.23 s) repp_stage_dbl_TCC3........................proved - complete [O]( 0.23 s) repp_stage_dbl_TCC4........................proved - complete [O]( 0.23 s) repp_stage_dbl_TCC5........................proved - complete [O]( 0.29 s) repp_stage_dbl_TCC6........................proved - complete [O]( 0.24 s) repp_stage_dbl.............................proved - complete [O](14.56 s) Theory totals: 32 formulas, 32 attempted, 32 succeeded (45.07 s) Proof summary for theory postnorm_impl postnorm_impl_TCC1..........................proved - complete [O](0.22 s) postnorm_impl_TCC2..........................proved - complete [O](0.23 s) postnorm_impl_TCC3..........................proved - complete [O](0.22 s) postnorm_impl_TCC4..........................proved - complete [O](0.23 s) postnorm_impl_correct1......................proved - complete [O](5.73 s) postnorm_impl_correct_siginx................proved - complete [O](0.41 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (7.04 s) Proof summary for theory sigrd_impl round_dec_impl_TCC1........................proved - complete [O]( 0.23 s) round_dec_impl_TCC2........................proved - complete [O]( 0.23 s) round_dec_impl_TCC3........................proved - complete [O]( 0.23 s) round_dec_impl_TCC4........................proved - complete [O]( 0.23 s) sigrd_impl_TCC1............................proved - complete [O]( 0.23 s) sigrd_impl_TCC2............................proved - complete [O]( 0.23 s) sigrd_impl_TCC3............................proved - complete [O]( 0.23 s) sigrd_impl_TCC4............................proved - complete [O]( 0.23 s) sigrd_impl_TCC5............................proved - complete [O]( 0.24 s) sigrd_impl_TCC6............................proved - complete [O]( 0.24 s) sigrd_impl_TCC7............................proved - complete [O]( 0.25 s) sigrd_impl_TCC8............................proved - complete [O]( 0.28 s) sigrd_impl_TCC9............................proved - complete [O]( 0.29 s) sigrd_impl_TCC10...........................proved - complete [O]( 0.28 s) sigrd_impl_TCC11...........................proved - complete [O]( 0.31 s) sigrd_impl_TCC12...........................proved - complete [O]( 0.31 s) sigrd_impl_TCC13...........................proved - complete [O]( 0.31 s) sigrd_impl_TCC14...........................proved - complete [O]( 0.31 s) sigrd_impl_TCC15...........................proved - complete [O]( 0.31 s) sigrd_impl_TCC16...........................proved - complete [O]( 0.31 s) sigrd_impl_TCC17...........................proved - complete [O]( 0.33 s) sigrd_impl_TCC18...........................proved - complete [O]( 0.32 s) round_dec_impl_correct_TCC1................proved - complete [O]( 0.23 s) round_dec_impl_correct.....................proved - complete [O]( 1.26 s) sigrd_impl_correct_double_TCC1.............proved - complete [O]( 0.29 s) sigrd_impl_correct_double_TCC2.............proved - complete [O]( 0.27 s) sigrd_impl_correct_double..................proved - complete [O](13.63 s) sigrd_impl_correct_single_TCC1.............proved - complete [O]( 0.25 s) sigrd_impl_correct_single_TCC2.............proved - complete [O]( 0.26 s) sigrd_impl_correct_single_TCC3.............proved - complete [O]( 0.29 s) sigrd_impl_correct_single_TCC4.............proved - complete [O]( 0.29 s) sigrd_impl_correct_single_TCC5.............proved - complete [O]( 0.29 s) sigrd_impl_correct_single_TCC6.............proved - complete [O]( 0.30 s) sigrd_impl_correct_single..................proved - complete [O](15.62 s) sigrd_impl_correct_sgl_lowbits_TCC1........proved - complete [O]( 0.23 s) sigrd_impl_correct_sgl_lowbits_TCC2........proved - complete [O]( 0.23 s) sigrd_impl_correct_sgl_lowbits_TCC3........proved - complete [O]( 0.24 s) sigrd_impl_correct_sgl_lowbits.............proved - complete [O]( 2.63 s) sigrd_impl_inx_correct_sgl.................proved - complete [O]( 7.65 s) sigrd_impl_inx_correct_dbl.................proved - complete [O](10.18 s) Theory totals: 40 formulas, 40 attempted, 40 succeeded (60.07 s) Proof summary for theory repp repp_impl_TCC1..............................proved - complete [O](0.23 s) repp_impl_TCC2..............................proved - complete [O](0.22 s) repp_impl_TCC3..............................proved - complete [O](0.26 s) repp_impl_TCC4..............................proved - complete [O](0.25 s) repp_impl_TCC5..............................proved - complete [O](0.26 s) repp_impl_TCC6..............................proved - complete [O](0.26 s) repp_impl_TCC7..............................proved - complete [O](0.28 s) repp_impl_TCC8..............................proved - complete [O](0.28 s) repp_impl_correct_single....................proved - complete [O](2.11 s) repp_impl_correct_double....................proved - complete [O](1.48 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (5.63 s) Proof summary for theory ns_impl ns_impl_passthrough........................proved - complete [O]( 0.31 s) ns_dom_lem_TCC1............................proved - complete [O]( 1.94 s) ns_dom_lem.................................proved - complete [O]( 8.98 s) ns_correct_tiny_ovf_sgl_TCC1...............proved - complete [O]( 0.22 s) ns_correct_tiny_ovf_sgl_TCC2...............proved - complete [O]( 0.22 s) ns_correct_tiny_ovf_sgl....................proved - complete [O]( 2.07 s) ns_correct_sgl_TCC1........................proved - complete [O]( 0.22 s) ns_correct_sgl_TCC2........................proved - complete [O]( 0.22 s) ns_correct_sgl_TCC3........................proved - complete [O]( 0.23 s) ns_correct_sgl_TCC4........................proved - complete [O]( 0.23 s) ns_correct_sgl_TCC5........................proved - complete [O]( 0.22 s) ns_correct_sgl_TCC6........................proved - complete [O]( 0.23 s) ns_correct_sgl_TCC7........................proved - complete [O]( 0.23 s) ns_correct_sgl_TCC8........................proved - complete [O]( 0.22 s) ns_correct_sgl_TCC9........................proved - complete [O]( 0.24 s) ns_correct_sgl_TCC10.......................proved - complete [O]( 0.32 s) ns_correct_sgl_TCC11.......................proved - complete [O]( 0.31 s) ns_correct_sgl_TCC12.......................proved - complete [O]( 0.24 s) ns_correct_sgl_TCC13.......................proved - complete [O]( 0.24 s) ns_correct_sgl_TCC14.......................proved - complete [O]( 0.39 s) ns_correct_sgl.............................proved - complete [O](27.34 s) ns_correct_tiny_ovf_dbl_TCC1...............proved - complete [O]( 0.22 s) ns_correct_tiny_ovf_dbl_TCC2...............proved - complete [O]( 0.22 s) ns_correct_tiny_ovf_dbl....................proved - complete [O]( 2.08 s) ns_correct_dbl_TCC1........................proved - complete [O]( 0.22 s) ns_correct_dbl_TCC2........................proved - complete [O]( 0.22 s) ns_correct_dbl_TCC3........................proved - complete [O]( 0.23 s) ns_correct_dbl_TCC4........................proved - complete [O]( 0.23 s) ns_correct_dbl_TCC5........................proved - complete [O]( 0.29 s) ns_correct_dbl_TCC6........................proved - complete [O]( 0.24 s) ns_correct_dbl.............................proved - complete [O](23.61 s) ns_impl_sign...............................proved - complete [O]( 0.29 s) Theory totals: 32 formulas, 32 attempted, 32 succeeded (72.47 s) Proof summary for theory flags_impl flags_ovf1_impl_TCC1.......................proved - complete [O]( 0.31 s) flags_ovf1_impl_TCC2.......................proved - complete [O]( 0.24 s) flags_ovf1_impl_TCC3.......................proved - complete [O]( 0.24 s) flags_ovf1_impl_TCC4.......................proved - complete [O]( 0.24 s) flags_ovf1_impl_TCC5.......................proved - complete [O]( 0.25 s) flags_ovf1_impl_TCC6.......................proved - complete [O]( 0.25 s) flags_ovf1_impl_TCC7.......................proved - complete [O]( 0.25 s) flags_ovf1_sgl_TCC1........................proved - complete [O]( 0.34 s) flags_ovf1_sgl_TCC2........................proved - complete [O]( 0.32 s) flags_ovf1_sgl_TCC3........................proved - complete [O]( 0.30 s) flags_ovf1_sgl_TCC4........................proved - complete [O]( 0.32 s) flags_ovf1_sgl.............................proved - complete [O]( 9.06 s) flags_ovf1_dbl_TCC1........................proved - complete [O]( 0.30 s) flags_ovf1_dbl_TCC2........................proved - complete [O]( 0.31 s) flags_ovf1_dbl.............................proved - complete [O](11.22 s) tiny_add_op1_sgl_TCC1......................proved - complete [O]( 0.22 s) tiny_add_op1_sgl...........................proved - complete [O]( 2.95 s) tiny_add_op1_dbl_TCC1......................proved - complete [O]( 0.23 s) tiny_add_op1_dbl...........................proved - complete [O]( 2.96 s) flags_lz_TCC1..............................proved - complete [O]( 0.22 s) flags_lz_TCC2..............................proved - complete [O]( 0.38 s) flags_impl_lz..............................proved - complete [O]( 0.63 s) flags_tiny_sgl.............................proved - complete [O]( 1.41 s) flags_tiny_dbl.............................proved - complete [O]( 1.77 s) Theory totals: 24 formulas, 24 attempted, 24 succeeded (34.72 s) Proof summary for theory expnorm_impl expn_const_sgl_TCC1........................proved - complete [O]( 0.24 s) expn_const_sgl.............................proved - complete [O](13.08 s) expn_const_dbl_TCC1........................proved - complete [O]( 0.26 s) expn_const_dbl.............................proved - complete [O](13.06 s) lz_negconst................................proved - complete [O]( 3.24 s) ns_expn_adds_impl_TCC1.....................proved - complete [O]( 0.27 s) ns_expn_adds_impl_TCC2.....................proved - complete [O]( 0.31 s) ns_expn_adds_impl_TCC3.....................proved - complete [O]( 0.34 s) ns_expn_adds_impl_TCC4.....................proved - complete [O]( 0.31 s) ns_expn_adds_impl_TCC5.....................proved - complete [O]( 0.34 s) ns_expn_adds_impl_sgl_TCC1.................proved - complete [O]( 0.40 s) ns_expn_adds_impl_sgl_TCC2.................proved - complete [O]( 0.36 s) ns_expn_adds_impl_sgl_TCC3.................proved - complete [O]( 1.72 s) ns_expn_adds_impl_sgl......................proved - complete [O](13.89 s) ns_expn_adds_impl_dbl_TCC1.................proved - complete [O]( 1.68 s) ns_expn_adds_impl_dbl......................proved - complete [O](11.66 s) ns_expnorm_corret_sgl_TCC1.................proved - complete [O]( 0.23 s) ns_expnorm_corret_sgl_TCC2.................proved - complete [O]( 0.36 s) ns_expnorm_corret_sgl_TCC3.................proved - complete [O]( 0.36 s) ns_expnorm_corret_sgl_TCC4.................proved - complete [O]( 0.36 s) ns_expnorm_corret_sgl_TCC5.................proved - complete [O]( 1.72 s) ns_expnorm_corret_sgl......................proved - complete [O]( 3.51 s) ns_expnorm_corret_dbl_TCC1.................proved - complete [O]( 0.23 s) ns_expnorm_corret_dbl_TCC2.................proved - complete [O]( 0.36 s) ns_expnorm_corret_dbl_TCC3.................proved - complete [O]( 1.66 s) ns_expnorm_corret_dbl......................proved - complete [O]( 2.67 s) ns_expn_incr_sgl_TCC1......................proved - complete [O]( 0.49 s) ns_expn_incr_sgl_TCC2......................proved - complete [O]( 0.49 s) ns_expn_incr_sgl...........................proved - complete [O]( 6.40 s) ns_expn_incr_dbl...........................proved - complete [O]( 4.38 s) Theory totals: 30 formulas, 30 attempted, 30 succeeded (84.38 s) Proof summary for theory shiftdist_impl TINY_small_exp.............................proved - complete [O]( 0.69 s) ns_shiftdist_sgl_TCC1......................proved - complete [O]( 0.25 s) ns_shiftdist_sgl...........................proved - complete [O]( 4.33 s) ns_shiftdist_dbl_TCC1......................proved - complete [O]( 0.24 s) ns_shiftdist_dbl...........................proved - complete [O](25.05 s) hibits_zero_sgl_TCC1.......................proved - complete [O]( 0.24 s) hibits_zero_sgl_TCC2.......................proved - complete [O]( 0.78 s) hibits_zero_sgl............................proved - complete [O]( 3.24 s) hibits_zero_dbl_TCC1.......................proved - complete [O]( 0.23 s) hibits_zero_dbl_TCC2.......................proved - complete [O]( 0.79 s) hibits_zero_dbl............................proved - complete [O]( 4.65 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (40.49 s) Proof summary for theory ns_shift signormshift_impl_TCC1.....................proved - complete [O]( 0.24 s) signormshift_impl_TCC2.....................proved - complete [O]( 0.23 s) signormshift_impl_TCC3.....................proved - complete [O]( 0.23 s) signormshift_impl_TCC4.....................proved - complete [O]( 0.52 s) signormshift_impl_TCC5.....................proved - complete [O]( 0.24 s) signormshift_correct_TCC1..................proved - complete [O]( 0.36 s) signormshift_correct_TCC2..................proved - complete [O]( 0.34 s) signormshift_correct_TCC3..................proved - complete [O]( 0.36 s) signormshift_correct_TCC4..................proved - complete [O]( 0.35 s) signormshift_correct_TCC5..................proved - complete [O]( 0.28 s) signormshift_correct_TCC6..................proved - complete [O]( 0.36 s) signormshift_correct_TCC7..................proved - complete [O]( 0.38 s) signormshift_correct_TCC8..................proved - complete [O]( 0.38 s) signormshift_correct_TCC9..................proved - complete [O]( 0.43 s) signormshift_correct_TCC10.................proved - complete [O]( 0.39 s) signormshift_correct_TCC11.................proved - complete [O]( 0.33 s) signormshift_correct_TCC12.................proved - complete [O]( 0.54 s) signormshift_correct.......................proved - complete [O](19.87 s) cls_func_ne0_TCC1..........................proved - complete [O]( 0.41 s) cls_func_ne0...............................proved - complete [O]( 2.26 s) signormshift_equiv.........................proved - complete [O](13.21 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (41.71 s) Proof summary for theory ns_mask mask_shP_impl_TCC1..........................proved - complete [O](0.23 s) mask_shP_impl_TCC2..........................proved - complete [O](0.24 s) mask_shP_impl_TCC3..........................proved - complete [O](0.26 s) mask_shP_impl_TCC4..........................proved - complete [O](0.26 s) mask_shP_impl_correct.......................proved - complete [O](4.62 s) mask_mask_impl_TCC1.........................proved - complete [O](0.27 s) mask_mask_impl_TCC2.........................proved - complete [O](0.28 s) mask_mask_impl_TCC3.........................proved - complete [O](0.24 s) mask_mask_impl_TCC4.........................proved - complete [O](0.26 s) mask_mask_impl_TCC5.........................proved - complete [O](0.26 s) mask_mask_impl_correct_TCC1.................proved - complete [O](0.46 s) mask_mask_impl_correct_TCC2.................proved - complete [O](0.26 s) mask_mask_impl_correct_TCC3.................proved - complete [O](0.46 s) mask_mask_impl_correct......................proved - complete [O](2.42 s) mask_correct_TCC1...........................proved - complete [O](0.35 s) mask_correct_TCC2...........................proved - complete [O](0.37 s) mask_correct_TCC3...........................proved - complete [O](0.28 s) mask_correct_TCC4...........................proved - complete [O](0.37 s) mask_correct_TCC5...........................proved - complete [O](0.38 s) mask_correct_TCC6...........................proved - complete [O](0.38 s) mask_correct_TCC7...........................proved - complete [O](0.46 s) mask_correct................................proved - complete [O](2.10 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (15.21 s) Proof summary for theory rd_input rounder_prerequesites_TCC1..................proved - complete [O](0.83 s) rounder_prerequesites_TCC2..................proved - complete [O](0.47 s) rd_inp_sign.................................proved - complete [O](1.58 s) adder_input_prereq_TCC1.....................proved - complete [O](0.24 s) add_input_ok_TCC1...........................proved - complete [O](0.84 s) add_input_ok_TCC2...........................proved - complete [O](0.42 s) add_input_ok_TCC3...........................proved - complete [O](0.40 s) add_input_ok................................proved - complete [O](7.32 s) muldiv_0xor1................................proved - complete [O](0.33 s) muldiv_input_ok_TCC1........................proved - complete [O](1.09 s) muldiv_input_ok_TCC2........................proved - complete [O](0.56 s) muldiv_input_ok_TCC3........................proved - complete [O](0.55 s) muldiv_input_ok.............................proved - complete [O](8.04 s) Theory totals: 13 formulas, 13 attempted, 13 succeeded (22.67 s) Proof summary for theory rd_import Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory val_bias Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory adjustexp_impl adjexp_ovf2_impl_TCC1.......................proved - complete [O](0.22 s) adjexp_ovf2_impl_TCC2.......................proved - complete [O](0.23 s) adjexp_ovf2_impl_TCC3.......................proved - complete [O](0.22 s) adjexp_ovf2_impl_TCC4.......................proved - complete [O](0.23 s) cons_correct_sgl_TCC1.......................proved - complete [O](0.59 s) cons_correct_sgl_TCC2.......................proved - complete [O](0.22 s) cons_correct_sgl............................proved - complete [O](1.35 s) cons_correct_dbl_TCC1.......................proved - complete [O](0.41 s) cons_correct_dbl_TCC2.......................proved - complete [O](0.22 s) cons_correct_dbl............................proved - complete [O](1.60 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (5.29 s) Proof summary for theory rd_stg rd_stg_composition..........................proved - complete [O](0.24 s) rd_double_flag..............................proved - complete [O](0.87 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.11 s) Proof summary for theory rounder Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Grand Totals: 461 proofs, 461 attempted, 461 succeeded (819.22 s)