Proof summary for theory fp_misc_stg Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory fp_misc_unpack fp_misc_unpack_TCC1.........................proved - complete [O](0.24 s) fp_misc_unpack_TCC2.........................proved - complete [O](0.25 s) fp_misc_unpack_TCC3.........................proved - complete [O](0.25 s) fp_misc_unpack_TCC4.........................proved - complete [O](0.24 s) fp_misc_unpack_TCC5.........................proved - complete [O](0.25 s) fp_misc_unpack_TCC6.........................proved - complete [O](0.25 s) fp_misc_unpack_TCC7.........................proved - complete [O](0.25 s) fp_misc_unpack_TCC8.........................proved - complete [O](0.26 s) fp_misc_unpack_TCC9.........................proved - complete [O](0.26 s) fp_misc_unpack_TCC10........................proved - complete [O](0.26 s) fp_misc_unpack_TCC11........................proved - complete [O](0.26 s) fp_misc_unpack_TCC12........................proved - complete [O](0.26 s) fp_misc_unpack_TCC13........................proved - complete [O](0.26 s) fp_misc_unpack_TCC14........................proved - complete [O](0.26 s) fp_misc_unpack_TCC15........................proved - complete [O](0.26 s) fp_misc_unpack_TCC16........................proved - complete [O](0.26 s) fp_misc_unpack_TCC17........................proved - complete [O](0.26 s) fp_misc_unpack_TCC18........................proved - complete [O](0.25 s) fp_misc_unpack_TCC19........................proved - complete [O](0.26 s) fp_misc_unpack_TCC20........................proved - complete [O](0.26 s) fp_misc_unpack_TCC21........................proved - complete [O](0.26 s) fp_misc_unpack_TCC22........................proved - complete [O](0.26 s) fp_misc_unpack_TCC23........................proved - complete [O](0.26 s) fp_misc_unpack_TCC24........................proved - complete [O](0.26 s) fp_misc_unpack_TCC25........................proved - complete [O](0.26 s) Theory totals: 25 formulas, 25 attempted, 25 succeeded (6.40 s) Proof summary for theory fp_rd2int rd2int_small_impl_TCC1.....................proved - complete [O]( 0.35 s) rd2int_small_impl_TCC2.....................proved - complete [O]( 0.35 s) rd2int_small_impl_TCC3.....................proved - complete [O]( 0.36 s) rd2int_small_impl_TCC4.....................proved - complete [O]( 0.36 s) rd2int_small_impl_TCC5.....................proved - complete [O]( 0.36 s) rd2int_small_impl_TCC6.....................proved - complete [O]( 0.37 s) rd2int_small_impl_TCC7.....................proved - complete [O]( 0.37 s) rd2int_small_impl_TCC8.....................proved - complete [O]( 0.37 s) rd2int_small_impl_TCC9.....................proved - complete [O]( 0.37 s) rd2int_small_tcc1_TCC1.....................proved - complete [O]( 0.25 s) rd2int_small_tcc1_TCC2.....................proved - complete [O]( 0.25 s) rd2int_small_tcc1..........................proved - complete [O]( 1.03 s) rd2int_small_tcc2..........................proved - complete [O]( 0.66 s) rd2int_small_tcc3_TCC1.....................proved - complete [O]( 0.24 s) rd2int_small_tcc3_TCC2.....................proved - complete [O]( 0.24 s) rd2int_small_tcc3..........................proved - complete [O]( 0.96 s) rd2int_small_tcc4..........................proved - complete [O]( 0.66 s) rd2int_small_sgl_TCC1......................proved - complete [O]( 1.72 s) rd2int_small_sgl_TCC2......................proved - complete [O]( 1.08 s) rd2int_small_sgl_TCC3......................proved - complete [O]( 0.56 s) rd2int_small_sgl_TCC4......................proved - complete [O]( 1.09 s) rd2int_small_sgl...........................proved - complete [O](29.65 s) rd2int_small_dbl_TCC1......................proved - complete [O]( 1.70 s) rd2int_small_dbl_TCC2......................proved - complete [O]( 1.10 s) rd2int_small_dbl_TCC3......................proved - complete [O]( 0.84 s) rd2int_small_dbl_TCC4......................proved - complete [O]( 1.10 s) rd2int_small_dbl...........................proved - complete [O](75.70 s) rd2int_small_int_impl_TCC1.................proved - complete [O]( 0.35 s) rd2int_small_int_impl_TCC2.................proved - complete [O]( 0.36 s) rd2int_small_int_impl_TCC3.................proved - complete [O]( 0.36 s) rd2int_small_int_impl_TCC4.................proved - complete [O]( 0.35 s) rd2int_small_int_impl_TCC5.................proved - complete [O]( 0.36 s) rd2int_small_int_impl_TCC6.................proved - complete [O]( 0.37 s) rd2int_small_int_impl_TCC7.................proved - complete [O]( 0.37 s) rd2int_small_int_impl_TCC8.................proved - complete [O]( 0.37 s) rd2int_small_int_impl_TCC9.................proved - complete [O]( 0.37 s) rd2int_small_int_impl_TCC10................proved - complete [O]( 0.38 s) rd2int_small_int_sgl_TCC1..................proved - complete [O]( 1.39 s) rd2int_small_int_sgl_TCC2..................proved - complete [O]( 0.93 s) rd2int_small_int_sgl.......................proved - complete [O](17.03 s) rd2int_small_int_dbl_TCC1..................proved - complete [O]( 1.38 s) rd2int_small_int_dbl_TCC2..................proved - complete [O]( 0.93 s) rd2int_small_int_dbl.......................proved - complete [O](13.44 s) rd2int_stg_TCC1............................proved - complete [O]( 0.29 s) rd2int_stg_TCC2............................proved - complete [O]( 0.28 s) rd2int_stg_TCC3............................proved - complete [O]( 0.30 s) rd2int_stg_corr_sgl........................proved - complete [O]( 2.14 s) rd2int_stg_corr_dbl........................proved - complete [O]( 2.24 s) rd2int_range_TCC1..........................proved - complete [O]( 0.28 s) rd2int_range_TCC2..........................proved - complete [O]( 0.29 s) rd2int_range_TCC3..........................proved - complete [O]( 0.30 s) rd2int_range_small.........................proved - complete [O]( 0.34 s) rd2int_range_sgl...........................proved - complete [O]( 1.09 s) rd2int_range_dbl...........................proved - complete [O]( 1.10 s) rd2int_extract_TCC1........................proved - complete [O]( 0.25 s) rd2int_extract_TCC2........................proved - complete [O]( 0.25 s) rd2int_extract_TCC3........................proved - complete [O]( 0.29 s) rd2int_extract_TCC4........................proved - complete [O]( 0.28 s) rd2int_extract_TCC5........................proved - complete [O]( 0.51 s) rd2int_extract_TCC6........................proved - complete [O]( 0.50 s) rd2int_extract_TCC7........................proved - complete [O]( 0.50 s) rd2int_extract_TCC8........................proved - complete [O]( 0.50 s) rd2int_extract_correct.....................proved - complete [O]( 8.08 s) rd2int_fmt_comb_TCC1.......................proved - complete [O]( 2.14 s) rd2int_sgl_dbl_TCC1........................proved - complete [O]( 0.53 s) rd2int_sgl_dbl_TCC2........................proved - complete [O]( 0.32 s) rd2int_sgl_dbl_TCC3........................proved - complete [O]( 0.32 s) rd2int_sgl_dbl_TCC4........................proved - complete [O]( 0.31 s) rd2int_sgl_dbl_TCC5........................proved - complete [O]( 0.31 s) rd2int_sgl_dbl.............................proved - complete [O]( 2.00 s) rd2int_fmt_correct_med_sgl_TCC1............proved - complete [O]( 0.57 s) rd2int_fmt_correct_med_sgl_TCC2............proved - complete [O]( 0.37 s) rd2int_fmt_correct_med_sgl_TCC3............proved - complete [O]( 0.25 s) rd2int_fmt_correct_med_sgl_TCC4............proved - complete [O]( 0.25 s) rd2int_fmt_correct_med_sgl_TCC5............proved - complete [O]( 0.52 s) rd2int_fmt_correct_med_sgl_TCC6............proved - complete [O]( 0.54 s) rd2int_fmt_correct_med_sgl_TCC7............proved - complete [O]( 0.25 s) rd2int_fmt_correct_med_sgl_TCC8............proved - complete [O]( 0.25 s) rd2int_fmt_correct_med_sgl.................proved - complete [O](30.25 s) rd2int_fmt_correct_med_dbl_TCC1............proved - complete [O]( 0.56 s) rd2int_fmt_correct_med_dbl_TCC2............proved - complete [O]( 0.39 s) rd2int_fmt_correct_med_dbl_TCC3............proved - complete [O]( 0.25 s) rd2int_fmt_correct_med_dbl_TCC4............proved - complete [O]( 0.23 s) rd2int_fmt_correct_med_dbl_TCC5............proved - complete [O]( 0.51 s) rd2int_fmt_correct_med_dbl_TCC6............proved - complete [O]( 0.53 s) rd2int_fmt_correct_med_dbl_TCC7............proved - complete [O]( 0.24 s) rd2int_fmt_correct_med_dbl_TCC8............proved - complete [O]( 0.26 s) rd2int_fmt_correct_med_dbl.................proved - complete [O](18.01 s) rd2int_fmt_correct_sgl_TCC1................proved - complete [O]( 0.37 s) rd2int_fmt_correct_sgl_TCC2................proved - complete [O]( 0.25 s) rd2int_fmt_correct_sgl_TCC3................proved - complete [O]( 0.25 s) rd2int_fmt_correct_sgl_TCC4................proved - complete [O]( 0.49 s) rd2int_fmt_correct_sgl_TCC5................proved - complete [O]( 0.51 s) rd2int_fmt_correct_sgl_TCC6................proved - complete [O]( 0.25 s) rd2int_fmt_correct_sgl_TCC7................proved - complete [O]( 0.25 s) rd2int_fmt_correct_sgl.....................proved - complete [O](24.94 s) rd2int_fmt_correct_dbl_TCC1................proved - complete [O]( 0.51 s) rd2int_fmt_correct_dbl_TCC2................proved - complete [O]( 0.25 s) rd2int_fmt_correct_dbl_TCC3................proved - complete [O]( 0.24 s) rd2int_fmt_correct_dbl_TCC4................proved - complete [O]( 0.66 s) rd2int_fmt_correct_dbl_TCC5................proved - complete [O]( 0.70 s) rd2int_fmt_correct_dbl_TCC6................proved - complete [O]( 0.27 s) rd2int_fmt_correct_dbl_TCC7................proved - complete [O]( 0.26 s) rd2int_fmt_correct_dbl.....................proved - complete [O](22.98 s) Theory totals: 104 formulas, 104 attempted, 104 succeeded (293.98 s) Proof summary for theory fp_compare_impl fp_compare_correct_sgl_TCC1................proved - complete [O]( 0.82 s) fp_compare_correct_sgl_TCC2................proved - complete [O]( 1.12 s) fp_compare_correct_sgl_TCC3................proved - complete [O]( 1.88 s) fp_compare_correct_sgl_TCC4................proved - complete [O]( 1.87 s) fp_compare_correct_sgl_TCC5................proved - complete [O]( 1.91 s) fp_compare_correct_sgl_TCC6................proved - complete [O]( 1.89 s) fp_compare_correct_sgl_TCC7................proved - complete [O]( 2.06 s) fp_compare_correct_sgl_TCC8................proved - complete [O]( 2.03 s) fp_compare_correct_sgl_TCC9................proved - complete [O]( 2.08 s) fp_compare_correct_sgl_TCC10...............proved - complete [O]( 2.08 s) fp_compare_correct_sgl.....................proved - complete [O](51.98 s) fp_compare_correct_dbl_TCC1................proved - complete [O]( 0.83 s) fp_compare_correct_dbl_TCC2................proved - complete [O]( 1.12 s) fp_compare_correct_dbl_TCC3................proved - complete [O]( 1.88 s) fp_compare_correct_dbl_TCC4................proved - complete [O]( 1.88 s) fp_compare_correct_dbl_TCC5................proved - complete [O]( 1.90 s) fp_compare_correct_dbl_TCC6................proved - complete [O]( 1.90 s) fp_compare_correct_dbl_TCC7................proved - complete [O]( 2.06 s) fp_compare_correct_dbl_TCC8................proved - complete [O]( 2.05 s) fp_compare_correct_dbl_TCC9................proved - complete [O]( 2.07 s) fp_compare_correct_dbl_TCC10...............proved - complete [O]( 2.07 s) fp_compare_correct_dbl.....................proved - complete [O](51.79 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (139.27 s) Proof summary for theory fp_misc_import Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory cvtd2s_lem cvtd2s_lem_TCC1.............................proved - complete [O](0.85 s) cvtd2s_lem_TCC2.............................proved - complete [O](0.89 s) cvtd2s_lem_TCC3.............................proved - complete [O](1.45 s) cvtd2s_lem..................................proved - complete [O](4.44 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (7.63 s) Proof summary for theory fp_misc_comb neg_correct1_TCC1..........................proved - complete [O]( 1.72 s) neg_correct1_TCC2..........................proved - complete [O]( 1.30 s) neg_correct1_TCC3..........................proved - complete [O]( 1.31 s) neg_correct1...............................proved - complete [O]( 0.80 s) abs_correct1_TCC1..........................proved - complete [O]( 1.41 s) abs_correct1_TCC2..........................proved - complete [O]( 1.37 s) abs_correct1...............................proved - complete [O]( 1.42 s) moves_correct1.............................proved - complete [O]( 2.43 s) cmp_sgl_correct_TCC1.......................proved - complete [O]( 2.56 s) cmp_sgl_correct_TCC2.......................proved - complete [O]( 0.42 s) cmp_sgl_correct_TCC3.......................proved - complete [O]( 0.35 s) cmp_sgl_correct_TCC4.......................proved - complete [O]( 0.31 s) cmp_sgl_correct............................proved - complete [O](28.51 s) cmp_dbl_correct_TCC1.......................proved - complete [O]( 0.36 s) cmp_dbl_correct_TCC2.......................proved - complete [O]( 0.42 s) cmp_dbl_correct_TCC3.......................proved - complete [O]( 0.30 s) cmp_dbl_correct_TCC4.......................proved - complete [O]( 0.42 s) cmp_dbl_correct............................proved - complete [O](23.59 s) cvts2i_correct_TCC1........................proved - complete [O]( 0.29 s) cvts2i_correct_TCC2........................proved - complete [O]( 0.67 s) cvts2i_correct_TCC3........................proved - complete [O]( 0.36 s) cvts2i_correct_TCC4........................proved - complete [O]( 0.38 s) cvts2i_correct_TCC5........................proved - complete [O]( 0.86 s) cvts2i_correct_TCC6........................proved - complete [O]( 1.05 s) cvts2i_correct_TCC7........................proved - complete [O]( 0.33 s) cvts2i_correct_TCC8........................proved - complete [O]( 0.36 s) cvts2i_correct.............................proved - complete [O](45.95 s) cvtd2i_correct_TCC1........................proved - complete [O]( 0.29 s) cvtd2i_correct_TCC2........................proved - complete [O]( 0.54 s) cvtd2i_correct_TCC3........................proved - complete [O]( 0.26 s) cvtd2i_correct_TCC4........................proved - complete [O]( 0.26 s) cvtd2i_correct_TCC5........................proved - complete [O]( 0.71 s) cvtd2i_correct_TCC6........................proved - complete [O]( 0.80 s) cvtd2i_correct_TCC7........................proved - complete [O]( 0.25 s) cvtd2i_correct_TCC8........................proved - complete [O]( 0.28 s) cvtd2i_correct.............................proved - complete [O](18.82 s) cvti2s_correct_TCC1........................proved - complete [O]( 0.27 s) cvti2s_correct_TCC2........................proved - complete [O]( 0.26 s) cvti2s_correct.............................proved - complete [O](61.62 s) cvti2d_correct.............................proved - complete [O](37.76 s) cvts2d_correct_TCC1........................proved - complete [O]( 0.31 s) cvts2d_correct_TCC2........................proved - complete [O]( 0.52 s) cvts2d_correct_TCC3........................proved - complete [O]( 0.25 s) cvts2d_correct_TCC4........................proved - complete [O]( 0.24 s) cvts2d_correct_TCC5........................proved - complete [O]( 0.24 s) cvts2d_correct_TCC6........................proved - complete [O]( 0.81 s) cvts2d_correct_TCC7........................proved - complete [O]( 0.74 s) cvts2d_correct_TCC8........................proved - complete [O]( 0.24 s) cvts2d_correct_TCC9........................proved - complete [O]( 0.25 s) cvts2d_correct_TCC10.......................proved - complete [O]( 0.25 s) cvts2d_correct_TCC11.......................proved - complete [O]( 1.62 s) cvts2d_correct.............................proved - complete [O](44.22 s) cvtd2s_correct_TCC1........................proved - complete [O]( 1.75 s) cvtd2s_correct_TCC2........................proved - complete [O]( 1.71 s) cvtd2s_correct_TCC3........................proved - complete [O]( 2.92 s) cvtd2s_correct_TCC4........................proved - complete [O]( 2.95 s) cvtd2s_correct_TCC5........................proved - complete [O]( 2.96 s) cvtd2s_correct_TCC6........................proved - complete [O]( 1.55 s) cvtd2s_correct_TCC7........................proved - complete [O]( 1.57 s) cvtd2s_correct_TCC8........................proved - complete [O]( 1.57 s) cvtd2s_correct_TCC9........................proved - complete [O]( 1.54 s) cvtd2s_correct_TCC10.......................proved - complete [O]( 1.53 s) cvtd2s_correct_TCC11.......................proved - complete [O]( 2.49 s) cvtd2s_correct_TCC12.......................proved - complete [O]( 2.41 s) cvtd2s_correct_TCC13.......................proved - complete [O]( 1.61 s) cvtd2s_correct_TCC14.......................proved - complete [O]( 1.61 s) cvtd2s_correct_TCC15.......................proved - complete [O]( 1.61 s) cvtd2s_correct_TCC16.......................proved - complete [O]( 1.61 s) cvtd2s_correct_TCC17.......................proved - complete [O]( 1.62 s) cvtd2s_correct_TCC18.......................proved - complete [O]( 1.62 s) cvtd2s_correct.............................proved - complete [O](63.17 s) Theory totals: 71 formulas, 71 attempted, 71 succeeded (388.86 s) Grand Totals: 226 proofs, 226 attempted, 226 succeeded (836.14 s)