Results from experiments... Result for In_dec FAILURE Result for Add_Equal FAILURE Result for equal_refl SUCCESS Result for equal_sym SUCCESS Result for equal_trans SUCCESS Result for subset_refl SUCCESS Result for subset_trans SUCCESS Result for subset_antisym SUCCESS Result for subset_equal SUCCESS Result for subset_empty FAILURE Result for subset_remove_3 FAILURE Result for subset_diff FAILURE Result for subset_add_3 FAILURE Result for subset_add_2 SUCCESS Result for in_subset SUCCESS Result for double_inclusion SUCCESS Result for empty_is_empty_1 FAILURE Result for empty_is_empty_2 FAILURE Result for add_equal FAILURE Result for add_add FAILURE Result for remove_equal FAILURE Result for Equal_remove FAILURE Result for add_remove FAILURE Result for remove_add FAILURE Result for singleton_equal_add FAILURE Result for remove_singleton_empty FAILURE Result for union_sym FAILURE Result for union_subset_equal FAILURE Result for union_equal_1 FAILURE Result for union_equal_2 FAILURE Result for union_assoc FAILURE Result for add_union_singleton FAILURE Result for union_add FAILURE Result for union_remove_add_1 FAILURE Result for union_remove_add_2 FAILURE Result for union_subset_1 SUCCESS Result for union_subset_2 SUCCESS Result for union_subset_3 FAILURE Result for union_subset_4 FAILURE Result for union_subset_5 FAILURE Result for empty_union_1 FAILURE Result for empty_union_2 FAILURE Result for not_in_union FAILURE Result for inter_sym FAILURE Result for inter_subset_equal FAILURE Result for inter_equal_1 FAILURE Result for inter_equal_2 FAILURE Result for inter_assoc FAILURE Result for union_inter_1 FAILURE Result for union_inter_2 FAILURE Result for inter_add_1 FAILURE Result for inter_add_2 FAILURE Result for empty_inter_1 FAILURE Result for empty_inter_2 FAILURE Result for inter_subset_1 FAILURE Result for inter_subset_2 FAILURE Result for inter_subset_3 SUCCESS Result for empty_diff_1 FAILURE Result for empty_diff_2 FAILURE Result for diff_subset FAILURE Result for diff_subset_equal FAILURE Result for remove_diff_singleton FAILURE Result for diff_inter_empty FAILURE Result for diff_inter_all FAILURE Result for Add_add FAILURE Result for Add_remove FAILURE Result for union_Add FAILURE Result for inter_Add FAILURE Result for union_Equal FAILURE Result for inter_Add_2 FAILURE Result for elements_Empty FAILURE Result for elements_empty FAILURE Result for of_list_1 FAILURE Result for of_list_2 FAILURE Result for of_list_3 FAILURE Result for fold_spec_right FAILURE Result for fold_rec FAILURE Result for fold_rec_bis FAILURE Result for fold_rec_nodep FAILURE Result for fold_rec_weak FAILURE Result for fold_rel FAILURE Result for set_induction FAILURE Result for set_induction_bis FAILURE Result for fold_identity FAILURE Result for fold_0 FAILURE Result for fold_1 FAILURE Result for fold_2 FAILURE Result for fold_1b FAILURE Result for fold_commutes FAILURE Result for fold_init FAILURE Result for fold_equal FAILURE Result for fold_empty FAILURE Result for fold_add FAILURE Result for add_fold FAILURE Result for remove_fold_1 FAILURE Result for remove_fold_2 FAILURE Result for fold_union_inter FAILURE Result for fold_diff_inter FAILURE Result for fold_union FAILURE Result for fold_plus FAILURE Result for cardinal_fold FAILURE Result for cardinal_0 FAILURE Result for cardinal_1 FAILURE Result for cardinal_2 FAILURE Result for cardinal_Empty FAILURE Result for cardinal_inv_1 FAILURE Result for cardinal_inv_2 FAILURE Result for cardinal_inv_2b FAILURE Result for Equal_cardinal FAILURE Result for empty_cardinal FAILURE Result for singleton_cardinal FAILURE Result for diff_inter_cardinal FAILURE Result for union_cardinal FAILURE Result for subset_cardinal FAILURE Result for subset_cardinal_lt FAILURE Result for union_inter_cardinal FAILURE Result for union_cardinal_inter FAILURE Result for union_cardinal_le FAILURE Result for add_cardinal_1 SUCCESS Result for add_cardinal_2 FAILURE Result for remove_cardinal_1 FAILURE Result for remove_cardinal_2 SUCCESS Result for sort_equivlistA_eqlistA FAILURE Result for gtb_1 FAILURE Result for leb_1 FAILURE Result for elements_split FAILURE Result for elements_Add FAILURE Result for elements_Add_Above FAILURE Result for elements_Add_Below FAILURE Result for set_induction_max FAILURE Result for set_induction_min FAILURE Result for fold_3 FAILURE Result for fold_4 FAILURE Result for fold_equal FAILURE Result for add_fold FAILURE Result for remove_fold_2 FAILURE Result for choose_equal FAILURE There were 15 out of 137 proven by Coq auto tactics On average, a proof was found automatically after 1781 milliseconds On average, a proof attempt took 4306 milliseconds