Results from experiments... Result for prop_congr FAILURE Result for is_true_true FAILURE Result for not_false_is_true SUCCESS Result for is_true_locked_true FAILURE Result for negbT FAILURE Result for negbTE FAILURE Result for negbF FAILURE Result for negbFE FAILURE Result for negbK FAILURE Result for negbNE FAILURE Result for negb_inj FAILURE Result for negbLR FAILURE Result for negbRL FAILURE Result for contra FAILURE Result for contraL FAILURE Result for contraR FAILURE Result for contraLR FAILURE Result for contraT FAILURE Result for wlog_neg FAILURE Result for contraFT FAILURE Result for contraFN FAILURE Result for contraTF FAILURE Result for contraNF FAILURE Result for contraFF FAILURE Result for ifP FAILURE Result for ifPn FAILURE Result for ifT FAILURE Result for ifF FAILURE Result for ifN FAILURE Result for if_same FAILURE Result for if_neg FAILURE Result for fun_if FAILURE Result for if_arg FAILURE Result for ifE SUCCESS Result for introNTF FAILURE Result for introTF FAILURE Result for elimNTF FAILURE Result for elimTF FAILURE Result for equivPif FAILURE Result for xorPif FAILURE Result for introTFn FAILURE Result for elimTFn FAILURE Result for equivPifn FAILURE Result for xorPifn FAILURE Result for introT FAILURE Result for introF FAILURE Result for introN FAILURE Result for introNf FAILURE Result for introTn FAILURE Result for introFn FAILURE Result for elimT FAILURE Result for elimF FAILURE Result for elimN FAILURE Result for elimNf FAILURE Result for elimTn FAILURE Result for elimFn FAILURE Result for introP FAILURE Result for iffP FAILURE Result for equivP FAILURE Result for sumboolP FAILURE Result for appP FAILURE Result for sameP FAILURE Result for decPcases FAILURE Result for rwP FAILURE Result for rwP2 FAILURE Result for altP FAILURE Result for bind_unless SUCCESS Result for unless_contra FAILURE Result for classicP FAILURE Result for classic_bind SUCCESS Result for classic_EM FAILURE Result for classic_imply FAILURE Result for classic_pick FAILURE Result for all_and2 SUCCESS Result for all_and3 SUCCESS Result for all_and4 SUCCESS Result for all_and5 SUCCESS Result for pair_andP SUCCESS Result for idP FAILURE Result for boolP FAILURE Result for idPn FAILURE Result for negP FAILURE Result for negPn FAILURE Result for negPf FAILURE Result for andP FAILURE Result for and3P FAILURE Result for and4P FAILURE Result for and5P FAILURE Result for orP FAILURE Result for or3P FAILURE Result for or4P FAILURE Result for nandP FAILURE Result for norP FAILURE Result for implyP FAILURE Result for andTb SUCCESS Result for andFb SUCCESS Result for andbT FAILURE Result for andbF FAILURE Result for andbb FAILURE Result for andbC SUCCESS Result for andbA SUCCESS Result for andbCA FAILURE Result for andbAC FAILURE Result for andbACA FAILURE Result for orTb SUCCESS Result for orFb SUCCESS Result for orbT FAILURE Result for orbF SUCCESS Result for orbb FAILURE Result for orbC SUCCESS Result for orbA SUCCESS Result for orbCA FAILURE Result for orbAC FAILURE Result for orbACA FAILURE Result for andbN SUCCESS Result for andNb SUCCESS Result for orbN SUCCESS Result for orNb SUCCESS Result for andb_orl FAILURE Result for andb_orr FAILURE Result for orb_andl FAILURE Result for orb_andr FAILURE Result for andb_idl FAILURE Result for andb_idr FAILURE Result for andb_id2l FAILURE Result for andb_id2r FAILURE Result for orb_idl FAILURE Result for orb_idr FAILURE Result for orb_id2l FAILURE Result for orb_id2r FAILURE Result for negb_and FAILURE Result for negb_or FAILURE Result for andbK FAILURE Result for andKb FAILURE Result for orbK FAILURE Result for orKb FAILURE Result for implybT FAILURE Result for implybF SUCCESS Result for implyFb SUCCESS Result for implyTb SUCCESS Result for implybb FAILURE Result for negb_imply FAILURE Result for implybE FAILURE Result for implyNb FAILURE Result for implybN FAILURE Result for implybNN FAILURE Result for implyb_idl FAILURE Result for implyb_idr FAILURE Result for implyb_id2l FAILURE Result for addFb SUCCESS Result for addbF FAILURE Result for addbb FAILURE Result for addbC FAILURE Result for addbA FAILURE Result for addbCA FAILURE Result for addbAC FAILURE Result for addbACA FAILURE Result for andb_addl FAILURE Result for andb_addr FAILURE Result for addKb FAILURE Result for addbK FAILURE Result for addIb FAILURE Result for addbI FAILURE Result for addTb SUCCESS Result for addbT FAILURE Result for addbN FAILURE Result for addNb FAILURE Result for addbP FAILURE Result for subrelUl FAILURE Result for subrelUr FAILURE Result for sub_refl SUCCESS Result for mem_topred FAILURE Result for topredE FAILURE Result for app_predE FAILURE Result for in_applicative FAILURE Result for in_collective FAILURE Result for in_simpl FAILURE Result for unfold_in SUCCESS Result for simpl_predE SUCCESS Result for mem_simpl SUCCESS Result for mem_mem FAILURE Result for qualifE SUCCESS Result for keyed_predE FAILURE Result for symmetric_from_pre FAILURE Result for sym_left_transitive FAILURE Result for sym_right_transitive FAILURE Result for equivalence_relP SUCCESS Result for rev_trans SUCCESS Result for forE SUCCESS Result for in1W SUCCESS Result for in2W SUCCESS Result for in3W SUCCESS Result for in1T SUCCESS Result for in2T SUCCESS Result for in3T SUCCESS Result for sub_in1 SUCCESS Result for sub_in11 SUCCESS Result for sub_in111 SUCCESS Result for on1W SUCCESS Result for on1lW SUCCESS Result for on2W SUCCESS Result for on1T SUCCESS Result for on1lT SUCCESS Result for on2T SUCCESS Result for subon1 SUCCESS Result for subon1l SUCCESS Result for subon2 SUCCESS Result for can_in_inj FAILURE Result for canLR_in FAILURE Result for canRL_in FAILURE Result for on_can_inj FAILURE Result for canLR_on FAILURE Result for canRL_on FAILURE Result for inW_bij FAILURE Result for onW_bij FAILURE Result for inT_bij FAILURE Result for onT_bij FAILURE Result for sub_in_bij SUCCESS Result for subon_bij SUCCESS Result for sub_in2 SUCCESS Result for sub_in3 SUCCESS Result for sub_in12 SUCCESS Result for sub_in21 SUCCESS Result for equivalence_relP_in SUCCESS Result for monoW FAILURE Result for mono2W FAILURE Result for homoRL FAILURE Result for homoLR FAILURE Result for homo_mono FAILURE Result for monoLR FAILURE Result for monoRL FAILURE Result for can_mono FAILURE Result for monoW_in FAILURE Result for mono2W_in FAILURE Result for homoRL_in FAILURE Result for homoLR_in FAILURE Result for homo_mono_in FAILURE Result for monoLR_in FAILURE Result for monoRL_in FAILURE Result for can_mono_in FAILURE There were 60 out of 240 proven by Coq auto tactics On average, a proof was found automatically after 725 milliseconds On average, a proof attempt took 749 milliseconds