Results from experiments... Result for mem_eq FAILURE Result for equal_mem_1 FAILURE Result for equal_mem_2 FAILURE Result for subset_mem_1 FAILURE Result for subset_mem_2 SUCCESS Result for empty_mem FAILURE Result for is_empty_equal_empty FAILURE Result for choose_mem_1 SUCCESS Result for choose_mem_2 SUCCESS Result for add_mem_1 SUCCESS Result for add_mem_2 FAILURE Result for remove_mem_1 FAILURE Result for remove_mem_2 FAILURE Result for singleton_equal_add SUCCESS Result for union_mem FAILURE Result for inter_mem FAILURE Result for diff_mem FAILURE Result for mem_3 FAILURE Result for mem_4 SUCCESS Result for equal_refl SUCCESS Result for equal_sym FAILURE Result for equal_trans SUCCESS Result for equal_equal FAILURE Result for equal_cardinal SUCCESS Result for subset_refl SUCCESS Result for subset_antisym SUCCESS Result for subset_trans SUCCESS Result for subset_equal SUCCESS Result for choose_mem_3 FAILURE Result for choose_mem_4 FAILURE Result for add_mem_3 SUCCESS Result for add_equal SUCCESS Result for remove_mem_3 SUCCESS Result for remove_equal FAILURE Result for add_remove FAILURE Result for remove_add FAILURE Result for is_empty_cardinal FAILURE Result for singleton_mem_1 SUCCESS Result for singleton_mem_2 FAILURE Result for singleton_mem_3 FAILURE Result for union_sym SUCCESS Result for union_subset_equal SUCCESS Result for union_equal_1 SUCCESS Result for union_equal_2 SUCCESS Result for union_assoc SUCCESS Result for add_union_singleton SUCCESS Result for union_add SUCCESS Result for union_subset_1 SUCCESS Result for union_subset_2 SUCCESS Result for union_subset_3 SUCCESS Result for inter_sym SUCCESS Result for inter_subset_equal SUCCESS Result for inter_equal_1 SUCCESS Result for inter_equal_2 SUCCESS Result for inter_assoc SUCCESS Result for union_inter_1 SUCCESS Result for union_inter_2 SUCCESS Result for inter_add_1 SUCCESS Result for inter_add_2 FAILURE Result for inter_subset_1 SUCCESS Result for inter_subset_2 SUCCESS Result for inter_subset_3 SUCCESS Result for diff_subset SUCCESS Result for diff_subset_equal SUCCESS Result for remove_inter_singleton SUCCESS Result for diff_inter_empty SUCCESS Result for diff_inter_all SUCCESS Result for set_rec FAILURE Result for exclusive_set FAILURE Result for fold_empty FAILURE Result for fold_equal 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 FAILURE Result for add_cardinal_1 SUCCESS Result for add_cardinal_2 FAILURE Result for remove_cardinal_1 FAILURE Result for remove_cardinal_2 FAILURE Result for union_cardinal FAILURE Result for subset_cardinal SUCCESS Result for filter_mem FAILURE Result for for_all_filter FAILURE Result for exists_filter FAILURE Result for partition_filter_1 SUCCESS Result for partition_filter_2 SUCCESS Result for filter_add_1 FAILURE Result for filter_add_2 FAILURE Result for add_filter_1 FAILURE Result for add_filter_2 FAILURE Result for union_filter FAILURE Result for filter_union FAILURE Result for for_all_mem_1 FAILURE Result for for_all_mem_2 FAILURE Result for for_all_mem_3 FAILURE Result for for_all_mem_4 FAILURE Result for for_all_exists FAILURE Result for exists_mem_1 FAILURE Result for exists_mem_2 FAILURE Result for exists_mem_3 FAILURE Result for exists_mem_4 FAILURE Result for sum_plus FAILURE Result for sum_filter FAILURE Result for fold_compat FAILURE Result for sum_compat FAILURE There were 47 out of 106 proven by Coq auto tactics On average, a proof was found automatically after 1401 milliseconds On average, a proof attempt took 5259 milliseconds