cF cHOL.False 22 66 120 1.61247043378
cT cHOL.True 22 111 112 1.687315746
cSUC cNat.Suc 27 165 370 1.3261613148
cCOND cHOL.If 16 370 575 1.30421856168
c<= cNat.ord_nat_inst.less_eq_nat 25 731 240 1.00022190852
c< cNat.ord_nat_inst.less_nat 18 299 365 1.11604826751
c+ cNat.plus_nat_inst.plus_nat 27 400 235 1.25668941282
cAPPEND cList.append 14 25 164 0.875427033704
cNIL cList.list.Nil 28 659 597 0.920883863644
cCONS cList.list.Cons 18 679 691 0.971888724446
c* cNat.times_nat_inst.times_nat 15 323 131 0.873240177835
c- cNat.minus_nat_inst.minus_nat 11 153 171 1.01584276404
cMAP cList.map 12 37 233 0.673740042003
cLAST cList.last 3 6 23 0.607085609083
cNULL cList.null 3 4 20 0.567315469791
cHD cList.hd 3 10 22 0.55528024125
cZIP cList.zip 4 6 65 0.523339971323
cTL cList.tl 3 11 30 0.516783850171
creal_sub cGroups.minus_class.minus 16 253 288 0.513355977449
creal_add cGroups.plus_class.plus 22 297 295 0.73329342435
creal_neg cGroups.uminus_class.uminus 17 132 184 0.63738036838
creal_mul cGroups.times_class.times 20 361 346 0.843430526055
creal_le cOrderings.ord_class.less_eq 24 948 831 0.582743789734
creal_lt cOrderings.ord_class.less 15 668 494 0.946997289544
creal_abs cGroups.abs_class.abs 13 201 74 0.621631280183
co cFun.comp 8 261 157 0.510789425305
creal_pow cPower.power_class.power 9 234 133 0.494107475846
cBUTLAST cList.butlast 3 3 24 0.471937565072
cREVERSE cList.rev 5 5 56 0.45788299964
cCURRY cProduct_Type.curry 1 1 10 0.402429604382
cdest_num cNat.Rep_Nat 1 1 10 0.402429604382
cmk_num cNat.Abs_Nat 2 2 10 0.325602649621
creal_div cFields.inverse_class.divide 4 150 157 0.317871342086
creal_sgn cGroups.sgn_class.sgn 2 22 18 0.334087703073
cFILTER cList.filter 5 16 78 0.306391737822
cALL2 cList.list_all2 2 13 73 0.291650878403
c__comma__ cProduct_Type.Pair 11 1700 1068 0.289112377437
cSND cProduct_Type.snd 3 20 77 0.408672824487
cFST cProduct_Type.fst 3 15 118 0.401076803989
cmk_pair cProduct_Type.Pair_Rep 1 5 3 0.352956123865
cUNCURRY cProduct_Type.internal_split 1 1 1 0.303413075542
cABS_prod cProduct_Type.Abs_prod 2 4 7 0.294160161472
cREP_prod cProduct_Type.Rep_prod 1 3 7 0.318928988904
cIND_0 cNat.Zero_Rep 3 5 7 0.283173658265
cIND_SUC cNat.Suc_Rep 4 6 9 0.497920105766
cNUM_REP cNat.Nat 2 4 17 0.470754911105
cI cFun.id 6 63 64 0.278028246817
c?! cHOL.Ex1 2 44 40 0.26758699444
creal_min cOrderings.ord_class.min 7 37 89 0.257196519721
cMOD cDivides.div_nat_inst.mod_nat 2 44 84 0.243440868845
cRTC cTransitive_Closure.rtranclp 6 46 42 0.234671286422
cFCONS cNat.nat.nat_case 1 3 29 0.222784809824
cREPLICATE cList.replicate 2 3 39 0.220868022573
cEXP cDivides.div_nat_inst.div_nat 2 204 56 0.214049188267
cvalue cInt.ring_1_class.of_int 4 16 34 0.211634904759
cre_compl cATP.fComp 1 2 5 0.201214802191
cINV cMeson.COMBC 1 5 2 0.201214802191
creal_max cOrderings.ord_class.max 6 45 89 0.195356118727
creal_of_num cNat.semiring_1_class.of_nat 8 1354 150 0.182292546094
cint_of_num cCode_Numeral.integer_of_nat 3 275 6 0.202511259208
cnum_of_int cCode_Numeral.nat_of_integer 1 10 9 0.221151427795
cITLIST cList.foldr 1 9 27 0.181776597594
cWF cOrderings.class.wellorder_axioms 1 36 8 0.176370547033
cNegation cInt.uminus_int_inst.uminus_int 1 4 87 0.170708673798
cpoly_add cList.splice 2 7 12 0.168374837012
cTC cTransitive_Closure.tranclp 5 41 31 0.167026890715
cCR cWellfounded.wfP 1 11 14 0.198025448362
cDELETE1 cList.remove1 3 17 31 0.166773283781
cLIST_UNIQ cList.linorder_class.sorted 3 18 49 0.22109359469
cMultiplication cInt.times_int_inst.times_int 1 6 134 0.149430287856
c__at__ cHilbert_Choice.Eps 2 50 21 0.143710198521
cWFP cWellfounded.accp 1 9 140 0.14004713622
cAddition cInt.plus_int_inst.plus_int 1 6 217 0.139407956165
cprime cNum.ring_1_class.iszero 1 96 19 0.133157865689
ctrivial_limit cPredicate.is_empty 1 28 13 0.169415910411
cone cSMT.pattern.Pattern 2 5 19 0.109296522196
cint_le cRings.dvd_class.dvd 2 138 189 0.102119543377
cint_mul cLattices.sup_class.sup 7 104 301 0.0889367855063
cint_add cLattices.inf_class.inf 5 124 284 0.211035986313
cIN cHOL.Let 1 2101 104 0.0813367284435
c_0 cNat.zero_nat_inst.zero_nat 3 3100 437 0.0750231852455
cPRE cNat.nat.nat_size 1 14 3 0.0660643424841
cBIT0 cNat.nat.size_nat_inst.size_nat 1 531 4 0.130514267632
cmirror cNum.num.Bit1 2 11 381 0.0643838843409
cminusinf cNum.BitM 1 11 17 0.190776089942
cplusinf cNum.num.Bit0 1 8 575 0.118564240113
cint_lt cRings.class.zero_neq_one 1 106 24 0.0637569785623
cEX cList.list_ex1 1 13 5 0.0594573783698
cradical cNum.neg_numeral_class.is_num 1 31 11 0.0570998158189
cdomain cMeson.skolem 1 1 4 0.0558110626551
chreal_of_num cCode_Numeral.natural_of_nat 2 14 33 0.054365239844
chreal_le cCode_Numeral.ord_natural_inst.less_eq_natural 1 20 41 0.148992651852
ccountable cString.enum_char_inst.enum_all_char 1 3 1 0.0517779112133
cmonoidal cGroups.semigroup 2 53 15 0.0449044343013
cALL cList.list_all 1 49 14 0.0382626384478
cint_ge cCode_Numeral.ord_integer_inst.less_eq_integer 1 6 15 0.0368585712991
cint_gt cCode_Numeral.ord_integer_inst.less_integer 1 10 52 0.0799019751334
cCOUNTABLE cString.enum_char_inst.enum_ex_char 1 114 1 0.0350612189874
cLET_END cQuickcheck_Narrowing.ensure_testable 1 17 1 0.0339623271895
c/__caret__ cATP.fconj 2 4302 9 0.0315533712445
cNUMERAL cSMT.fun_app 1 3099 1 0.031096538895
c__caret__/ cATP.fdisj 1 503 9 0.0237578887435
cpoly_neg cList.rotate1 1 4 11 0.0217657713804
cpoly_diff cList.remdups_adj 1 5 24 0.0416317909804
cInd cOrderings.top_class.top 4 6 296 0.0176884116042
cBool cOrderings.bot_class.bot 4 17 612 0.132237411661
cpoly_diff_aux cList.rotate 1 5 16 0.0113463093958
cpoly_cmul cList.removeAll 1 7 14 0.0120637356084
cUr_bool cGroups.one_class.one 2 7 249 0.0101725468403
cUr_ind cGroups.zero_class.zero 2 7 560 0.140997864331
cINL cSum_Type.Inl 3 10 78 0.00471521974602
cOUTL cSum_Type.Projl 1 1 2 0.721347520444
cINR cSum_Type.Inr 3 10 82 0.149166626121
cOUTR cSum_Type.Projr 1 1 2 0.721347520444
cONE cExtraction.sumbool.Left 2 4 22 0.00253978996132
cTOP cExtraction.sumbool.Right 1 6 23 0.202361869694
cZBOT cCode_Numeral.pcr_natural 1 6 19 0.00077913819972
cZRECSPACE cTransfer.right_unique 1 5 24 0.0520397387256
cSN cEquiv_Relations.equivp 1 12 21 0.000342679909742
cWN cEquiv_Relations.part_equivp 1 5 14 0.116913498993
cmk_ind cString.char_of_nat 1 2 5 0.000276393959053
cdest_ind cString.nat_of_char 1 2 266 0.15922563253
cmk_I cString.nibble_of_nat 1 2 24 0.00018563705057
cdest_I cString.nat_of_nibble 1 2 24 0.255622218635
cOr cNum.plus_num_inst.plus_num 0 8 52 0.
cPERMUTATION cList.distinct 0 9 79 0.
creal_open cEnum.enum_class.enum_ex 0 14 13 0.
cINFINITE cEnum.enum_class.enum_all 0 41 13 0.
cBOTTOM cLazy_Sequence.empty 0 3 45 0.
cclosed_in cSet.Ball 0 148 295 0.
cdepth cNat.size_class.size 0 7 269 0.
cint_sub cDivides.div_class.mod 0 69 73 0.
cint_sgn cCode_Numeral.uminus_integer_inst.uminus_integer 0 20 14 0.
cint_neg cCode_Numeral.sgn_integer_inst.sgn_integer 0 90 6 0.
cint_abs cCode_Numeral.abs_integer_inst.abs_integer 0 74 10 0.
cAnd cNum.times_num_inst.times_num 0 7 34 0.
cABORT cPredicate.seq.Empty 0 5 42 0.
copen_in cSet.Bex 0 198 163 0.