Proof summary for theory min_array imin_TCC1...................................proved - complete [O](0.81 s) min_TCC1....................................proved - complete [O](0.18 s) min_lem.....................................proved - complete [O](0.10 s) min_in?.....................................proved - complete [O](0.13 s) min_def.....................................proved - complete [O](0.26 s) min_it_is...................................proved - complete [O](0.28 s) imin_lem....................................proved - complete [O](0.22 s) imin_1......................................proved - complete [O](0.10 s) min_2_TCC1..................................proved - complete [O](0.05 s) min_2_TCC2..................................proved - complete [O](0.06 s) min_2.......................................proved - complete [O](0.33 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.52 s) Proof summary for theory max_array imax_TCC1...................................proved - complete [O](0.25 s) max_TCC1....................................proved - complete [O](0.19 s) max_lem.....................................proved - complete [O](0.09 s) max_in?.....................................proved - complete [O](0.13 s) imax_lem....................................proved - complete [O](0.21 s) max_def.....................................proved - complete [O](0.15 s) max_it_is...................................proved - complete [O](0.26 s) imax_1......................................proved - complete [O](0.09 s) max_2_TCC1..................................proved - complete [O](0.06 s) max_2_TCC2..................................proved - complete [O](0.06 s) max_2.......................................proved - complete [O](0.30 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.79 s) Proof summary for theory sort_array_lems sort_min_TCC1...............................proved - complete [O](0.04 s) sort_min....................................proved - complete [O](0.45 s) sort_max_TCC1...............................proved - complete [O](0.05 s) sort_max....................................proved - complete [O](0.51 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.05 s) Proof summary for theory array_ops caret_fill0_TCC1............................proved - complete [O](0.20 s) caret_fill0_TCC2............................proved - complete [O](0.25 s) caret_fill0_TCC3............................proved - complete [O](0.31 s) caret_fill0.................................proved - complete [O](1.02 s) caret_fill1.................................proved - complete [O](1.00 s) caret_concat_bot_TCC1.......................proved - complete [O](0.07 s) caret_concat_bot_TCC2.......................proved - complete [O](0.27 s) caret_concat_bot............................proved - complete [O](5.66 s) caret_concat_top_TCC1.......................proved - complete [O](0.18 s) caret_concat_top_TCC2.......................proved - complete [O](0.26 s) caret_concat_top_TCC3.......................proved - complete [O](0.27 s) caret_concat_top_TCC4.......................proved - complete [O](0.37 s) caret_concat_top_TCC5.......................proved - complete [O](0.29 s) caret_concat_top............................proved - complete [O](1.71 s) caret_concat_all_TCC1.......................proved - complete [O](0.08 s) caret_concat_all_TCC2.......................proved - complete [O](0.07 s) caret_concat_all_TCC3.......................proved - complete [O](0.07 s) caret_concat_all_TCC4.......................proved - complete [O](0.08 s) caret_concat_all_TCC5.......................proved - complete [O](0.06 s) caret_concat_all_TCC6.......................proved - complete [O](0.03 s) caret_concat_all_TCC7.......................proved - complete [O](0.10 s) caret_concat_all............................proved - complete [O](0.67 s) array_decomp_TCC1...........................proved - complete [O](0.06 s) array_decomp_TCC2...........................proved - complete [O](0.05 s) array_decomp_TCC3...........................proved - complete [O](0.03 s) array_decomp_TCC4...........................proved - complete [O](0.04 s) array_decomp_TCC5...........................proved - complete [O](0.07 s) array_decomp................................proved - complete [O](1.28 s) caret_bot_all_TCC1..........................proved - complete [O](0.06 s) caret_bot_all_TCC2..........................proved - complete [O](0.06 s) caret_bot_all...............................proved - complete [O](0.52 s) caret_top_all_TCC1..........................proved - complete [O](0.19 s) caret_top_all_TCC2..........................proved - complete [O](0.24 s) caret_top_all...............................proved - complete [O](1.33 s) concat_array_bot_TCC1.......................proved - complete [O](0.06 s) concat_array_bot............................proved - complete [O](0.15 s) concat_array_top_TCC1.......................proved - complete [O](0.07 s) concat_array_top_TCC2.......................proved - complete [O](0.05 s) concat_array_top............................proved - complete [O](0.37 s) concat_array_r..............................proved - complete [O](0.15 s) concat_array_l..............................proved - complete [O](0.18 s) concat_array_assoc..........................proved - complete [O](0.47 s) Theory totals: 42 formulas, 42 attempted, 42 succeeded (18.45 s) Proof summary for theory caret_arrays caret_TCC1..................................proved - complete [O](0.11 s) caret_TCC2..................................proved - complete [O](0.06 s) caret_TCC3..................................proved - complete [O](0.22 s) caret_TCC4..................................proved - complete [O](0.06 s) caret_TCC5..................................proved - complete [O](0.07 s) caret_TCC6..................................proved - complete [O](0.27 s) caret_TCC7..................................proved - complete [O](0.16 s) caret_all_TCC1..............................proved - complete [O](0.07 s) caret_all_TCC2..............................proved - complete [O](0.04 s) caret_all...................................proved - complete [O](0.31 s) caret_ii_0_TCC1.............................proved - complete [O](0.05 s) caret_ii_0..................................proved - complete [O](0.19 s) caret_elim_TCC1.............................proved - complete [O](0.26 s) caret_elim_TCC2.............................proved - complete [O](0.26 s) caret_elim..................................proved - complete [O](0.27 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (2.40 s) Proof summary for theory empty_array_def empty_array_TCC1............................proved - complete [O](0.07 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.07 s) Proof summary for theory concat_arrays oh_TCC1.....................................proved - complete [O](0.06 s) oh_TCC2.....................................proved - complete [O](0.16 s) concat_array_bot0_TCC1......................proved - complete [O](0.08 s) concat_array_bot0...........................proved - complete [O](0.23 s) concat_array_top0_TCC1......................proved - complete [O](0.07 s) concat_array_top0...........................proved - complete [O](0.22 s) concat_array_bot_TCC1.......................proved - complete [O](0.13 s) concat_array_bot............................proved - complete [O](0.07 s) concat_array_top_TCC1.......................proved - complete [O](0.12 s) concat_array_top_TCC2.......................proved - complete [O](0.06 s) concat_array_top............................proved - complete [O](0.07 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.27 s) Proof summary for theory majority_array is_majority_TCC1............................proved - complete [O](0.08 s) maj_TCC1....................................proved - complete [O](0.54 s) is_majority_unique..........................proved - complete [O](0.96 s) maj_lem.....................................proved - complete [O](0.13 s) maj_subset..................................proved - complete [O](0.46 s) maj_in_array................................proved - complete [O](0.38 s) is_majority_const...........................proved - complete [O](0.21 s) maj_const...................................proved - complete [O](0.08 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (2.84 s) Proof summary for theory majority_seq is_majority_TCC1............................proved - complete [O](0.09 s) maj_TCC1....................................proved - complete [O](0.21 s) is_majority_unique..........................proved - complete [O](1.00 s) maj_lem.....................................proved - complete [O](0.13 s) maj_subset..................................proved - complete [O](0.55 s) maj_in_seq..................................proved - complete [O](0.40 s) length_eq_1_TCC1............................proved - complete [O](0.05 s) length_eq_1.................................proved - complete [O](0.37 s) is_majority_const...........................proved - complete [O](0.33 s) maj_const...................................proved - complete [O](0.07 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (3.20 s) Proof summary for theory max_seq Imax_TCC1...................................proved - complete [O](0.11 s) Imax_TCC2...................................proved - complete [O](0.07 s) Imax_TCC3...................................proved - complete [O](2.07 s) Imax_1_TCC1.................................proved - complete [O](0.05 s) Imax_1......................................proved - complete [O](0.20 s) imax_TCC1...................................proved - complete [O](0.55 s) max_TCC1....................................proved - complete [O](0.33 s) max_seq_lem.................................proved - complete [O](0.11 s) max_seq_in?.................................proved - complete [O](0.16 s) imax_seq_lem................................proved - complete [O](0.23 s) max_seq_def.................................proved - complete [O](0.14 s) max_seq_it_is...............................proved - complete [O](0.31 s) imax_seq_1..................................proved - complete [O](0.11 s) max_seq_2_TCC1..............................proved - complete [O](0.05 s) max_seq_2_TCC2..............................proved - complete [O](0.10 s) max_seq_2...................................proved - complete [O](0.35 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (4.94 s) Proof summary for theory seqs Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory min_seq Imin_TCC1...................................proved - complete [O](0.12 s) Imin_TCC2...................................proved - complete [O](0.28 s) Imin_TCC3...................................proved - complete [O](2.05 s) Imin_seq_1_TCC1.............................proved - complete [O](0.05 s) Imin_seq_1..................................proved - complete [O](0.21 s) imin_TCC1...................................proved - complete [O](0.55 s) min_TCC1....................................proved - complete [O](0.32 s) min_seq_lem.................................proved - complete [O](0.11 s) min_seq_in?.................................proved - complete [O](0.16 s) min_seq_def.................................proved - complete [O](0.14 s) min_seq_it_is...............................proved - complete [O](0.32 s) imin_seq_lem................................proved - complete [O](0.25 s) imin_seq_1..................................proved - complete [O](0.12 s) min_seq_2_TCC1..............................proved - complete [O](0.05 s) min_seq_2_TCC2..............................proved - complete [O](0.10 s) min_seq_2...................................proved - complete [O](0.39 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (5.22 s) Proof summary for theory sort_array sort_TCC1...................................proved - complete [O](0.33 s) sort_lem....................................proved - complete [O](0.07 s) sort_in?....................................proved - complete [O](0.15 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.55 s) Proof summary for theory sort_array_def swap_TCC1...................................proved - complete [O](0.06 s) swap_TCC2...................................proved - complete [O](0.21 s) asort_TCC1..................................proved - complete [O](0.13 s) asort_TCC2..................................proved - complete [O](0.06 s) swap_perm...................................proved - complete [O](1.76 s) asort_perm..................................proved - complete [O](0.35 s) swap_P_and_Q_TCC1...........................proved - complete [O](0.09 s) swap_P_and_Q................................proved - complete [O](2.80 s) asort_P_and_Q...............................proved - complete [O](1.15 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (6.61 s) Proof summary for theory min_array_def ge_total....................................proved - complete [O](0.30 s) IMP_max_array_def_TCC1......................proved - complete [O](0.05 s) Imin_TCC1...................................proved - complete [O](0.07 s) Imin_TCC2...................................proved - complete [O](0.83 s) Imin_1_TCC1.................................proved - complete [O](0.05 s) Imin_1......................................proved - complete [O](0.18 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.48 s) Proof summary for theory max_array_def imax_rec_TCC1...............................proved - complete [O](0.07 s) imax_rec_TCC2...............................proved - complete [O](0.06 s) imax_rec_lem................................proved - complete [O](1.07 s) imax_rec_rng................................proved - complete [O](0.52 s) Imax_rec_TCC1...............................proved - complete [O](0.06 s) Imax_rec_TCC2...............................proved - complete [O](0.11 s) Imax_TCC1...................................proved - complete [O](0.07 s) Imax_TCC2...................................proved - complete [O](0.42 s) Imax_1_TCC1.................................proved - complete [O](0.10 s) Imax_1......................................proved - complete [O](0.16 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (2.64 s) Proof summary for theory below_arrays Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory permutations perm_reflexive..............................proved - complete [O](0.33 s) perm_symmetric..............................proved - complete [O](0.53 s) perm_tran...................................proved - complete [O](0.56 s) perm_in?....................................proved - complete [O](0.29 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.71 s) Proof summary for theory permutations_seq perm_length.................................proved - complete [O](1.13 s) perm_reflexive..............................proved - complete [O](0.37 s) perm_symmetric..............................proved - complete [O](1.15 s) perm_tran...................................proved - complete [O](0.66 s) perm_in?....................................proved - complete [O](0.33 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (3.64 s) Proof summary for theory sort_seq increasing?_TCC1............................proved - complete [O](0.16 s) sort_TCC1...................................proved - complete [O](1.13 s) sort_length.................................proved - complete [O](0.13 s) sort_seq_lem................................proved - complete [O](0.08 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.50 s) Proof summary for theory top Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Grand Totals: 186 proofs, 186 attempted, 186 succeeded (61.88 s)