Results from experiments... Result for bits_lt_antirefl FAILURE Result for bits_lt_trans FAILURE Result for compare_spec FAILURE Result for mem_spec SUCCESS Result for mem_Leaf FAILURE Result for empty_spec FAILURE Result for mem_node FAILURE Result for is_empty_spec FAILURE Result for subset_Leaf_s FAILURE Result for subset_spec FAILURE Result for equal_subset FAILURE Result for equal_spec FAILURE Result for eq_dec FAILURE Result for lex_Opp FAILURE Result for compare_bool_inv FAILURE Result for compare_inv FAILURE Result for lex_Eq FAILURE Result for compare_bool_Eq FAILURE Result for compare_equal FAILURE Result for compare_gt FAILURE Result for compare_eq FAILURE Result for compare_spec FAILURE Result for ct_cxe FAILURE Result for ct_xce FAILURE Result for ct_lxl FAILURE Result for ct_gxg FAILURE Result for ct_xll FAILURE Result for ct_xgg FAILURE Result for ct_lex FAILURE Result for ct_compare_bool FAILURE Result for compare_x_Leaf FAILURE Result for compare_empty_x FAILURE Result for compare_x_empty FAILURE Result for ct_compare FAILURE Result for add_spec FAILURE Result for remove_spec FAILURE Result for singleton_spec FAILURE Result for union_spec FAILURE Result for inter_spec FAILURE Result for diff_spec FAILURE Result for fold_spec FAILURE Result for cardinal_spec FAILURE Result for xfilter_spec FAILURE Result for filter_spec FAILURE Result for xforall_spec FAILURE Result for for_all_spec FAILURE Result for xexists_spec FAILURE Result for exists_spec FAILURE Result for partition_filter FAILURE Result for partition_spec1 FAILURE Result for partition_spec2 FAILURE Result for xelements_spec FAILURE Result for elements_spec1 FAILURE Result for lt_rev_append FAILURE Result for elements_spec2 FAILURE Result for elements_spec2w FAILURE Result for choose_spec1 FAILURE Result for choose_spec2 FAILURE Result for choose_empty FAILURE Result for choose_spec3' FAILURE Result for choose_spec3 FAILURE Result for min_elt_spec1 FAILURE Result for min_elt_spec3 FAILURE Result for min_elt_spec2 FAILURE Result for max_elt_spec1 FAILURE Result for max_elt_spec3 FAILURE Result for max_elt_spec2 FAILURE There were 1 out of 67 proven by Coq auto tactics On average, a proof was found automatically after 376 milliseconds On average, a proof attempt took 985 milliseconds