Proof summary for theory alpha_sticky sticky_TCC1.................................proved - complete [O](0.09 s) sticky_TCC2.................................proved - complete [O](0.09 s) sticky_TCC3.................................proved - complete [O](0.09 s) sticky_comp_TCC1............................proved - complete [O](0.09 s) sticky_comp_TCC2............................proved - complete [O](0.09 s) sticky_comp_TCC3............................proved - complete [O](0.09 s) sticky_comp_TCC4............................proved - complete [O](0.09 s) sticky_comp.................................proved - complete [O](3.06 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (3.69 s) Proof summary for theory fp_compare relation_cover..............................proved - complete [O](0.59 s) relation_exclusive..........................proved - complete [O](0.86 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.45 s) Proof summary for theory compare_comp compare_lem................................proved - complete [O]( 2.60 s) less_compute...............................proved - complete [O](15.25 s) equal_compute..............................proved - complete [O]( 1.75 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (19.60 s) Proof summary for theory bv2fact f_TCC1......................................proved - complete [O](0.10 s) bv2fact_real_fprec..........................proved - complete [O](0.24 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.34 s) Proof summary for theory factoring_misc ff_fact_coarsen.............................proved - complete [O](4.61 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (4.61 s) Proof summary for theory fpop_result result_correct_TCC1.........................proved - complete [O](0.13 s) result_correct_TCC2.........................proved - complete [O](0.16 s) result_correct_TCC3.........................proved - complete [O](0.16 s) result_correct_TCC4.........................proved - complete [O](0.22 s) result_correct_TCC5.........................proved - complete [O](0.18 s) result_correct_TCC6.........................proved - complete [O](0.19 s) result_correct_TCC7.........................proved - complete [O](0.26 s) result_correct_TCC8.........................proved - complete [O](0.19 s) result_correct_TCC9.........................proved - complete [O](0.21 s) result_correct_TCC10........................proved - complete [O](0.34 s) result_correct_TCC11........................proved - complete [O](0.17 s) result_correct_TCC12........................proved - complete [O](0.17 s) result_correct_TCC13........................proved - complete [O](0.27 s) result_correct_TCC14........................proved - complete [O](0.20 s) result_correct_TCC15........................proved - complete [O](0.20 s) result_correct_TCC16........................proved - complete [O](0.35 s) result_correct_TCC17........................proved - complete [O](0.21 s) result_correct_TCC18........................proved - complete [O](0.22 s) result_correct_TCC19........................proved - complete [O](0.32 s) result_correct_TCC20........................proved - complete [O](0.21 s) result_correct_TCC21........................proved - complete [O](0.21 s) result_correct_TCC22........................proved - complete [O](0.34 s) result_correct_TCC23........................proved - complete [O](0.54 s) result_correct_TCC24........................proved - complete [O](0.55 s) result_correct_TCC25........................proved - complete [O](0.84 s) result_correct_equiv_TCC1...................proved - complete [O](0.09 s) result_correct_equiv_TCC2...................proved - complete [O](0.09 s) result_correct_equiv_TCC3...................proved - complete [O](0.09 s) result_correct_equiv_TCC4...................proved - complete [O](0.09 s) result_correct_equiv_TCC5...................proved - complete [O](0.35 s) result_correct_equiv........................proved - complete [O](2.77 s) result_correct_0............................proved - complete [O](4.04 s) Theory totals: 32 formulas, 32 attempted, 32 succeeded (14.36 s) Proof summary for theory inx INX_TCC1....................................proved - complete [O](0.09 s) INX_eq......................................proved - complete [O](1.34 s) INX_ovf_wrapped.............................proved - complete [O](2.32 s) INX_UNF.....................................proved - complete [O](0.21 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (3.96 s) Proof summary for theory ieee_specials STD_QNAN_is_qnan_s_TCC1.....................proved - complete [O](0.09 s) STD_QNAN_is_qnan_s_TCC2.....................proved - complete [O](0.09 s) STD_QNAN_is_qnan_s_TCC3.....................proved - complete [O](0.08 s) STD_QNAN_is_qnan_s..........................proved - complete [O](0.71 s) STD_QNAN_is_qnan_d_TCC1.....................proved - complete [O](0.09 s) STD_QNAN_is_qnan_d_TCC2.....................proved - complete [O](0.08 s) STD_QNAN_is_qnan_d_TCC3.....................proved - complete [O](0.08 s) STD_QNAN_is_qnan_d..........................proved - complete [O](0.72 s) STDs_QNAN_is_qnan_s.........................proved - complete [O](0.94 s) STDs_QNAN_is_qnan_d.........................proved - complete [O](0.89 s) INF_is_inf_s................................proved - complete [O](0.71 s) INF_is_inf_d................................proved - complete [O](0.69 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (5.17 s) Proof summary for theory ieee_embed NP_judg1....................................proved - complete [O](0.09 s) NP_judg2....................................proved - complete [O](0.11 s) bv2ieee_bv_TCC1.............................proved - complete [O](0.09 s) bv2ieee_bv_TCC2.............................proved - complete [O](0.10 s) bv2ieee_bv_TCC3.............................proved - complete [O](0.12 s) bv2ieee_bv_TCC4.............................proved - complete [O](0.20 s) bv2ieee_bv_TCC5.............................proved - complete [O](0.09 s) ieee_bv2bv_TCC1.............................proved - complete [O](0.10 s) ieee_bv2bv_TCC2.............................proved - complete [O](0.13 s) ieee_bv2bv_TCC3.............................proved - complete [O](0.10 s) ieee_bv2bv_TCC4.............................proved - complete [O](0.12 s) ieee_bv_vv..................................proved - complete [O](4.23 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (5.48 s) Proof summary for theory ieee_bv ieee_bv_TCC1................................proved - complete [O](0.10 s) q_nan?_TCC1.................................proved - complete [O](0.14 s) ieeebv2fact_TCC1............................proved - complete [O](0.13 s) signed_inf_is_inf...........................proved - complete [O](0.13 s) qs_nan_is_nan...............................proved - complete [O](0.16 s) zero_iff_zero...............................proved - complete [O](2.95 s) ieeebv2fact_is_representable1...............proved - complete [O](4.73 s) ieeebv2fact_is_representable2...............proved - complete [O](0.47 s) ieeebv2fact_is_representable3...............proved - complete [O](0.13 s) special_xors................................proved - complete [O](0.58 s) special_cover...............................proved - complete [O](0.16 s) ieee_if_zero_or_nonz........................proved - complete [O](0.11 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (9.79 s) Proof summary for theory biased_int value_bias_TCC1.............................proved - complete [O](0.54 s) bias_convert_TCC1...........................proved - complete [O](0.09 s) bias_convert_TCC2...........................proved - complete [O](0.19 s) bias_convert_TCC3...........................proved - complete [O](0.19 s) bias_convert_TCC4...........................proved - complete [O](0.18 s) bias_convert_TCC5...........................proved - complete [O](0.19 s) bias_convert................................proved - complete [O](2.13 s) value_bias_bij..............................proved - complete [O](0.17 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (3.68 s) Proof summary for theory ieee_shortcuts Sbv2ieee_bv_TCC1............................proved - complete [O](0.09 s) Sbv2ieee_bv_TCC2............................proved - complete [O](0.09 s) Sbv2ieee_bv_TCC3............................proved - complete [O](0.09 s) Dbv2ieee_bv_TCC1............................proved - complete [O](0.09 s) Dbv2ieee_bv_TCC2............................proved - complete [O](0.09 s) Dbv2ieee_bv_TCC3............................proved - complete [O](0.08 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.53 s) Proof summary for theory rd2int IMP_fact_mul2_TCC1.........................proved - complete [O]( 0.09 s) Ngt1.......................................proved - complete [O]( 0.09 s) rd2int_lem1................................proved - complete [O]( 1.52 s) rd2int_lem2................................proved - complete [O]( 3.18 s) rd2int_rewr_TCC1...........................proved - complete [O]( 0.18 s) rd2int_rewr................................proved - complete [O]( 2.05 s) rd2int_is_int..............................proved - complete [O]( 0.43 s) rd2int_pos_correct.........................proved - complete [O]( 1.29 s) rd2int_neg_correct.........................proved - complete [O]( 0.97 s) rd2int_zero_correct........................proved - complete [O]( 8.06 s) rd2int_nearest_correct.....................proved - complete [O]( 1.23 s) rd2int_tie_TCC1............................proved - complete [O]( 0.12 s) rd2int_tie.................................proved - complete [O]( 0.95 s) rd2int_large...............................proved - complete [O]( 4.77 s) rd2int_small_TCC1..........................proved - complete [O]( 0.58 s) rd2int_small_TCC2..........................proved - complete [O]( 0.28 s) rd2int_small...............................proved - complete [O](13.69 s) rd2int_alg1_TCC1...........................proved - complete [O]( 0.09 s) rd2int_alg1................................proved - complete [O]( 0.73 s) rd2int_alg2................................proved - complete [O]( 0.69 s) rd2int_format_TCC1.........................proved - complete [O]( 1.64 s) rd2int_format..............................proved - complete [O]( 1.64 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (44.27 s) Proof summary for theory wrapped_exp rd_result_TCC1..............................proved - complete [O](0.09 s) eta_wrapped_ovf.............................proved - complete [O](3.12 s) eta_wrapped_unf.............................proved - complete [O](1.69 s) eta_e_wrapped...............................proved - complete [O](1.93 s) eta_f_wrapped...............................proved - complete [O](1.59 s) eta_ovf_after...............................proved - complete [O](3.29 s) eta_rd_result...............................proved - complete [O](3.64 s) rd_result_small.............................proved - complete [O](1.87 s) rd_result_eq................................proved - complete [O](1.03 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (18.25 s) Proof summary for theory ovf_unf TINY_rep....................................proved - complete [O](0.55 s) TINY_eq.....................................proved - complete [O](1.16 s) LOSS_TCC1...................................proved - complete [O](0.08 s) LOSS_rep....................................proved - complete [O](0.32 s) LOSS_eq.....................................proved - complete [O](0.27 s) LOSS_sigrd_TCC1.............................proved - complete [O](0.10 s) LOSS_sigrd..................................proved - complete [O](1.66 s) LOSS_mode_indep.............................proved - complete [O](0.16 s) UNFeq.......................................proved - complete [O](0.43 s) ovf_emax....................................proved - complete [O](0.65 s) OVF_e_emax..................................proved - complete [O](0.21 s) OVF_before_eq...............................proved - complete [O](0.18 s) OVF_before_rep..............................proved - complete [O](0.15 s) OVF_before_impl.............................proved - complete [O](1.27 s) OVF_after_eq................................proved - complete [O](0.46 s) OVF_after_rep...............................proved - complete [O](0.15 s) OVF_decomp..................................proved - complete [O](0.26 s) not_OVF_before_and_after....................proved - complete [O](0.10 s) ovf_eq......................................proved - complete [O](0.20 s) ovf_rep.....................................proved - complete [O](0.16 s) not_TINY_and_OVF............................proved - complete [O](0.23 s) OVF_after_impl..............................proved - complete [O](0.45 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (9.20 s) Proof summary for theory sigrd_props ceil_lem...................................proved - complete [O]( 1.27 s) floor_lem..................................proved - complete [O]( 1.39 s) sigrd_impl_lem.............................proved - complete [O](19.58 s) sigrd_repr_TCC1............................proved - complete [O]( 0.10 s) sigrd_repr_TCC2............................proved - complete [O]( 0.11 s) sigrd_repr_TCC3............................proved - complete [O]( 0.11 s) sigrd_repr.................................proved - complete [O]( 0.62 s) sigrd_fact_eq..............................proved - complete [O]( 0.97 s) fact_decomposition.........................proved - complete [O]( 0.29 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (24.44 s) Proof summary for theory round_props round_inx_TCC1..............................proved - complete [O](0.09 s) round_inx...................................proved - complete [O](2.46 s) round_inx_eq................................proved - complete [O](0.38 s) round_denormal..............................proved - complete [O](1.55 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (4.48 s) Proof summary for theory round_fact2 rnd_repr_l1................................proved - complete [O]( 0.17 s) rnd_repr__l1...............................proved - complete [O]( 3.18 s) rnd_repr__l2...............................proved - complete [O](14.05 s) rnd_repr___l3a.............................proved - complete [O]( 2.54 s) rnd_repr___l3b.............................proved - complete [O]( 1.16 s) rnd_repr_lem_TCC1..........................proved - complete [O]( 0.23 s) rnd_repr_lem...............................proved - complete [O]( 9.87 s) rnd_repr_TCC1..............................proved - complete [O]( 0.20 s) rnd_repr...................................proved - complete [O]( 1.60 s) rnd_equiv..................................proved - complete [O]( 0.34 s) rnd_repr_hat_TCC1..........................proved - complete [O]( 0.19 s) rnd_repr_hat...............................proved - complete [O]( 0.26 s) rnd_equiv_hat..............................proved - complete [O]( 0.38 s) alpha_rep_real_fprec.......................proved - complete [O]( 1.91 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (36.08 s) Proof summary for theory alpha_rd_lem eta_hat_equiv1..............................proved - complete [O](1.27 s) eta_hat_equiv2..............................proved - complete [O](0.30 s) eta_hat_equiv...............................proved - complete [O](0.19 s) etahat_equiv_commute........................proved - complete [O](0.38 s) eta_equiv0..................................proved - complete [O](2.82 s) eta_equiv1..................................proved - complete [O](2.48 s) eta_equiv2..................................proved - complete [O](0.33 s) eta_equiv...................................proved - complete [O](0.28 s) alpha_rep_log1_TCC1.........................proved - complete [O](0.15 s) alpha_rep_log1..............................proved - complete [O](0.78 s) alpha_rep_log2_TCC1.........................proved - complete [O](0.15 s) alpha_rep_log2..............................proved - complete [O](7.76 s) alpha_rep_eta...............................proved - complete [O](1.36 s) alpha_rep_ii_fact_TCC1......................proved - complete [O](0.13 s) alpha_rep_ii_fact...........................proved - complete [O](0.49 s) alpha_eq_normshift..........................proved - complete [O](0.74 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (19.61 s) Proof summary for theory alpha_lemmas alpha_neg...................................proved - complete [O](0.23 s) alpha_rep_neg...............................proved - complete [O](1.72 s) alpha_stretch_TCC1..........................proved - complete [O](0.11 s) alpha_stretch...............................proved - complete [O](2.12 s) alpha_shrink................................proved - complete [O](2.09 s) alpha_shrink_stretch_TCC1...................proved - complete [O](0.12 s) alpha_shrink_stretch........................proved - complete [O](0.26 s) alpha_rep_shrink_stretch....................proved - complete [O](8.00 s) alpha_transl................................proved - complete [O](0.31 s) alpha_refine_l1.............................proved - complete [O](0.56 s) alpha_refine................................proved - complete [O](0.13 s) alpha_sign..................................proved - complete [O](1.56 s) alpha_ge0...................................proved - complete [O](0.57 s) alpha_eq0...................................proved - complete [O](0.16 s) alpha_eq_sign...............................proved - complete [O](0.16 s) alpha_abs...................................proved - complete [O](0.16 s) alpha_rep_small.............................proved - complete [O](0.21 s) alpha_rep_large.............................proved - complete [O](0.82 s) alpha_eq_smaller............................proved - complete [O](0.16 s) alpha_eq_abs................................proved - complete [O](0.21 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (19.66 s) Proof summary for theory alpha_equiv alpha_q_TCC1................................proved - complete [O](0.62 s) alpha_q_uniq................................proved - complete [O](0.15 s) alpha_eq_is_equiv...........................proved - complete [O](1.39 s) alpha_rep_eq................................proved - complete [O](0.49 s) alpha_singl_xor_intv........................proved - complete [O](0.22 s) alpha_rep_is_rep_l1.........................proved - complete [O](0.40 s) alpha_rep_is_rep............................proved - complete [O](1.58 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (4.85 s) Proof summary for theory round_monoton round_neg_over_representable_TCC1...........proved - complete [O](0.36 s) round_neg_over_representable................proved - complete [O](0.37 s) round_nearest_over_representable............proved - complete [O](0.36 s) round_over_representable....................proved - complete [O](0.91 s) round_under_representable_TCC1..............proved - complete [O](0.27 s) round_under_representable...................proved - complete [O](0.40 s) round_Xmin_TCC1.............................proved - complete [O](0.27 s) round_Xmin..................................proved - complete [O](0.13 s) round_minus_Xmin_TCC1.......................proved - complete [O](0.23 s) round_minus_Xmin............................proved - complete [O](0.15 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (3.45 s) Proof summary for theory xmin Xmin_fact_TCC1..............................proved - complete [O](0.09 s) Xmin_fact_TCC2..............................proved - complete [O](0.52 s) Xmin_TCC1...................................proved - complete [O](0.35 s) Xmin_val....................................proved - complete [O](0.81 s) Xmin_gaps...................................proved - complete [O](0.26 s) Xmin_mininal................................proved - complete [O](0.23 s) Xmin_mininal_abs............................proved - complete [O](0.16 s) Xmin_multiples..............................proved - complete [O](1.66 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (4.08 s) Proof summary for theory round_correct round_is_representable_TCC1................proved - complete [O]( 0.08 s) round_is_representable.....................proved - complete [O]( 0.16 s) round_pos_correct_l1.......................proved - complete [O]( 6.57 s) round_pos_correct..........................proved - complete [O]( 2.50 s) round_neg_correct..........................proved - complete [O]( 4.16 s) round_zero_correct.........................proved - complete [O]( 5.41 s) round_nearest_correct......................proved - complete [O]( 2.73 s) round_nearest_correct_tie..................proved - complete [O](10.39 s) round_fix..................................proved - complete [O]( 0.49 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (32.49 s) Proof summary for theory round_decomposition sigrd_TCC_lem..............................proved - complete [O]( 7.47 s) sigrd_TCC1.................................proved - complete [O]( 0.21 s) sigrd_rewr_TCC1............................proved - complete [O]( 0.11 s) sigrd_rewr.................................proved - complete [O]( 0.35 s) sigrd_lem1.................................proved - complete [O](26.88 s) postnorm_TCC_lem_TCC1......................proved - complete [O]( 0.10 s) postnorm_TCC_lem_TCC2......................proved - complete [O]( 0.11 s) postnorm_TCC_lem_TCC3......................proved - complete [O]( 0.24 s) postnorm_TCC_lem...........................proved - complete [O]( 1.46 s) postnorm_TCC1..............................proved - complete [O]( 6.99 s) ii_postnorm_val_TCC1.......................proved - complete [O]( 0.09 s) ii_postnorm_val............................proved - complete [O]( 6.51 s) ii_round_decomposition_p...................proved - complete [O]( 4.08 s) ii_round_decomposition_TCC1................proved - complete [O]( 0.09 s) ii_round_decomposition_TCC2................proved - complete [O]( 0.09 s) ii_round_decomposition.....................proved - complete [O]( 0.13 s) eta_e_round................................proved - complete [O]( 0.16 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (55.07 s) Proof summary for theory round_frac rd_to_nearest_TCC1.........................proved - complete [O]( 0.18 s) rd_to_nearest_neg..........................proved - complete [O]( 6.27 s) round_to_even1.............................proved - complete [O]( 0.87 s) round_to_even2.............................proved - complete [O]( 1.55 s) round_to_even3_l1..........................proved - complete [O]( 1.70 s) round_to_even3_TCC1........................proved - complete [O]( 0.14 s) round_to_even3.............................proved - complete [O]( 0.25 s) round_l0...................................proved - complete [O]( 0.72 s) round_l1...................................proved - complete [O]( 0.62 s) round_l2...................................proved - complete [O]( 0.94 s) round_TCC1.................................proved - complete [O]( 0.17 s) round_even_distance........................proved - complete [O]( 2.27 s) round_even_tie.............................proved - complete [O]( 7.25 s) round_pos_neg_refl.........................proved - complete [O]( 0.65 s) round_pos_neg_refl2........................proved - complete [O]( 0.14 s) round_neg_pos_refl.........................proved - complete [O]( 0.13 s) round_pos_neg_zero.........................proved - complete [O]( 0.50 s) round_nearest_neg..........................proved - complete [O]( 0.57 s) round_nearest_refl.........................proved - complete [O]( 0.14 s) round_sign.................................proved - complete [O](12.77 s) round_0....................................proved - complete [O]( 0.13 s) round_zero_neg.............................proved - complete [O]( 0.45 s) round_zero_refl............................proved - complete [O]( 0.11 s) Theory totals: 23 formulas, 23 attempted, 23 succeeded (38.52 s) Proof summary for theory add_zero ge_le_zero..................................proved - complete [O](0.75 s) add_zero_TCC1...............................proved - complete [O](0.09 s) add_zero....................................proved - complete [O](0.49 s) add_Xmin....................................proved - complete [O](0.64 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.97 s) Proof summary for theory eta_props eta_hat_e...................................proved - complete [O](0.17 s) eta_e_TCC1..................................proved - complete [O](0.13 s) eta_e.......................................proved - complete [O](0.39 s) eta_e_neg...................................proved - complete [O](0.61 s) eta_hat_f...................................proved - complete [O](0.29 s) eta_f.......................................proved - complete [O](1.36 s) eta_f_neg...................................proved - complete [O](0.70 s) eta_nor.....................................proved - complete [O](1.41 s) eta_denor...................................proved - complete [O](1.69 s) etahat_value_TCC1...........................proved - complete [O](0.15 s) etahat_value................................proved - complete [O](2.53 s) eta_value1..................................proved - complete [O](1.28 s) eta_value2..................................proved - complete [O](0.87 s) eta_hat_e_expt..............................proved - complete [O](0.12 s) eta_unique1.................................proved - complete [O](0.15 s) eta_unique2.................................proved - complete [O](0.13 s) eta_unique3.................................proved - complete [O](0.24 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (12.22 s) Proof summary for theory fact_props ff_norm_e...................................proved - complete [O](1.76 s) fact_exp_monoton1...........................proved - complete [O](2.07 s) fact_exp_monoton2...........................proved - complete [O](4.30 s) fact_exp_monoton3...........................proved - complete [O](0.12 s) fact_exp_minsize............................proved - complete [O](0.75 s) factoring_minus_TCC1........................proved - complete [O](0.12 s) factoring_minus.............................proved - complete [O](0.15 s) factoring_unique_sign.......................proved - complete [O](0.48 s) factoring_unique_same_expt..................proved - complete [O](1.38 s) factoring_add_0_same_expt...................proved - complete [O](0.61 s) i3e_factoring_unique_expt...................proved - complete [O](0.19 s) i3e_factoring_unique........................proved - complete [O](0.67 s) i3e_factoring_add_0.........................proved - complete [O](1.54 s) Theory totals: 13 formulas, 13 attempted, 13 succeeded (14.14 s) Proof summary for theory fin_exponent ff_is_if_judg...............................proved - complete [O](0.20 s) Xmax_fact_TCC1..............................proved - complete [O](0.30 s) Xmax_fact_TCC2..............................proved - complete [O](0.09 s) Xmax_fact_TCC3..............................proved - complete [O](1.30 s) Xmax_val....................................proved - complete [O](0.19 s) Xmax_posreal................................proved - complete [O](0.26 s) Xmax_expt_emax..............................proved - complete [O](0.25 s) Xmax_gt_emax................................proved - complete [O](0.51 s) ff_maxval...................................proved - complete [O](0.58 s) factoring_neg_ff_i3e_number.................proved - complete [O](0.75 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (4.43 s) Proof summary for theory fin_precision if_max_f....................................proved - complete [O](1.21 s) if_max_intv.................................proved - complete [O](1.01 s) if_max_intv2................................proved - complete [O](1.31 s) if_gaps0....................................proved - complete [O](0.16 s) if_gaps1....................................proved - complete [O](3.14 s) if_gaps2....................................proved - complete [O](5.85 s) if_gaps3....................................proved - complete [O](0.57 s) factoring_neg_if_i3e_number.................proved - complete [O](0.51 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (13.76 s) Proof summary for theory eta eta_hat_TCC1................................proved - complete [O](0.12 s) eta_hat_TCC2................................proved - complete [O](0.31 s) eta_hat_correct.............................proved - complete [O](0.16 s) eta_TCC1....................................proved - complete [O](0.28 s) eta_correct.................................proved - complete [O](0.19 s) eta_hat_eta_TCC1............................proved - complete [O](0.22 s) eta_hat_eta.................................proved - complete [O](0.63 s) eta_hat_le_eta..............................proved - complete [O](0.36 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (2.27 s) Proof summary for theory factoring sig_nor_den.................................proved - complete [O](0.12 s) fac_nor_den.................................proved - complete [O](0.17 s) sign_TCC1...................................proved - complete [O](0.08 s) sign_TCC2...................................proved - complete [O](0.08 s) val_zero....................................proved - complete [O](0.93 s) zero_fact_TCC1..............................proved - complete [O](0.09 s) zero_fact_val...............................proved - complete [O](0.19 s) val_factoring_0.............................proved - complete [O](0.17 s) val_factoring_0_rev.........................proved - complete [O](0.16 s) factoring_neg_TCC1..........................proved - complete [O](0.11 s) factoring_neg_value.........................proved - complete [O](0.16 s) i3e_nor.....................................proved - complete [O](0.70 s) i3e_denor...................................proved - complete [O](0.73 s) factoring_neg_ii_i3e_number.................proved - complete [O](0.32 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (4.01 s) Proof summary for theory enumerated_type_defs pos_sign_rep_judg...........................proved - complete [O](0.08 s) neg_sign_rep_judg...........................proved - complete [O](0.09 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.17 s) Proof summary for theory konstanten emax_TCC1...................................proved - complete [O](0.10 s) emin_TCC1...................................proved - complete [O](0.12 s) bias_TCC1...................................proved - complete [O](0.22 s) emin_vs_emax................................proved - complete [O](0.17 s) Alpha_TCC1..................................proved - complete [O](0.18 s) emin_emax_Alpha.............................proved - complete [O](0.92 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.71 s) Proof summary for theory ieee_import Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory fact_norm f_norm_lem..................................proved - complete [O](1.33 s) f_normalize_TCC1............................proved - complete [O](0.11 s) f_normalize_TCC2............................proved - complete [O](0.13 s) f_norm_corr.................................proved - complete [O](0.20 s) i3e_normalize_TCC1..........................proved - complete [O](0.12 s) i3e_normalize_TCC2..........................proved - complete [O](0.10 s) i3e_normalize_TCC3..........................proved - complete [O](2.06 s) i3e_norm_corr...............................proved - complete [O](0.78 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (4.83 s) Proof summary for theory fact_mul2 if_fact_mul2................................proved - complete [O](3.83 s) if_i3e_number_eta_minus.....................proved - complete [O](0.13 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (3.96 s) Proof summary for theory rd_result_props rd_result_0.................................proved - complete [O](0.22 s) rd_result_pos_neg_refl......................proved - complete [O](1.12 s) rd_result_neg_pos_refl......................proved - complete [O](1.12 s) rd_result_nearest_refl......................proved - complete [O](1.90 s) rd_result_zero_refl.........................proved - complete [O](1.92 s) round_gt_0_rd_result_gt_0_TCC1..............proved - complete [O](0.25 s) round_gt_0_rd_result_gt_0...................proved - complete [O](1.94 s) round_lt_0_rd_result_lt_0_TCC1..............proved - complete [O](0.25 s) round_lt_0_rd_result_lt_0...................proved - complete [O](0.58 s) rd_result_sum_gt_0..........................proved - complete [O](0.37 s) rd_result_sum_lt_0..........................proved - complete [O](0.44 s) rd_result_diff_gt_0.........................proved - complete [O](0.23 s) rd_result_diff_lt_0.........................proved - complete [O](0.21 s) Theory totals: 13 formulas, 13 attempted, 13 succeeded (10.55 s) Proof summary for theory ieee Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Grand Totals: 397 proofs, 397 attempted, 397 succeeded (461.13 s)