{{"aloul-chnl11-13.cnf",UNS,2505.85},{"een-pico-prop01-75.cnf",UNS,5.62},{"een-pico-prop05-50.cnf",UNS,61.15},{"een-tip-sat-nusmv-t5.B.cnf",SAT,9.79},{"een-tip-sat-nusmv-tt5.B.cnf",SAT,10.06},{"een-tip-uns-nusmv-t5.B.cnf",UNS,2.54},{"goldb-heqc-alu4mul.cnf",UNS,824.13},{"goldb-heqc-dalumul.cnf",UNK,3600.00},{"goldb-heqc-desmul.cnf",UNS,57.25},{"goldb-heqc-frg2mul.cnf",UNS,373.41},{"goldb-heqc-i10mul.cnf",UNK,3600.00},{"goldb-heqc-i8mul.cnf",UNS,678.93},{"goldb-heqc-term1mul.cnf",UNK,3600.00},{"grieu-vmpc-s05-25.cnf",SAT,133.50},{"grieu-vmpc-s05-27.cnf",SAT,146.50},{"grieu-vmpc-s05-28.cnf",UNK,3600.00},{"grieu-vmpc-s05-34.cnf",UNK,3600.00},{"hoons-vbmc-lucky7.cnf",UNS,24.90},{"ibm-2002-05r-k90.cnf",SAT,51.75},{"ibm-2002-07r-k100.cnf",UNS,145.24},{"ibm-2002-11r1-k45.cnf",SAT,225.00},{"ibm-2002-19r-k100.cnf",UNK,3600.00},{"ibm-2002-21r-k95.cnf",UNK,3600.00},{"ibm-2002-26r-k45.cnf",UNS,2.07},{"ibm-2002-27r-k95.cnf",SAT,15.91},{"ibm-2004-03-k70.cnf",SAT,61.81},{"ibm-2004-04-k100.cnf",SAT,645.20},{"ibm-2004-06-k90.cnf",SAT,590.70},{"ibm-2004-1_11-k25.cnf",UNS,8.00},{"ibm-2004-1_31_2-k25.cnf",UNS,107.18},{"ibm-2004-19-k90.cnf",UNK,3600.00},{"ibm-2004-2_02_1-k100.cnf",UNS,17.47},{"ibm-2004-2_14-k45.cnf",UNS,19.05},{"ibm-2004-26-k25.cnf",UNS,0.94},{"ibm-2004-3_02_1-k95.cnf",UNS,2.72},{"ibm-2004-3_02_3-k95.cnf",SAT,2.45},{"ibm-2004-3_11-k60.cnf",UNK,3600.00},{"ibm-2004-6_02_3-k100.cnf",UNS,10.38},{"manol-pipe-c10id_s.cnf",UNS,106.12},{"manol-pipe-c10nidw_s.cnf",UNK,3600.00},{"manol-pipe-c6nidw_i.cnf",UNS,666.22},{"manol-pipe-c7b.cnf",UNS,49.47},{"manol-pipe-c7b_i.cnf",UNS,60.20},{"manol-pipe-c7bidw_i.cnf",UNK,3600.00},{"manol-pipe-c7nidw.cnf",UNK,3600.00},{"manol-pipe-c9.cnf",UNS,8.85},{"manol-pipe-c9nidw_s.cnf",UNS,1666.90},{"manol-pipe-f10ni.cnf",UNK,3600.00},{"manol-pipe-f6bi.cnf",UNS,14.76},{"manol-pipe-f7idw.cnf",UNS,2162.77},{"manol-pipe-f9b.cnf",UNK,3600.00},{"manol-pipe-f9n.cnf",UNK,3600.00},{"manol-pipe-g10b.cnf",UNS,164.75},{"manol-pipe-g10bidw.cnf",UNK,3600.00},{"manol-pipe-g10id.cnf",UNS,199.21},{"manol-pipe-g10nid.cnf",UNK,3600.00},{"manol-pipe-g6bi.cnf",UNS,2.38},{"manol-pipe-g7nidw.cnf",UNS,43.36},{"maris-s03-gripper11.cnf",SAT,824.00},{"mizh-md5-47-3.cnf",SAT,162.87},{"mizh-md5-47-4.cnf",SAT,112.02},{"mizh-md5-47-5.cnf",SAT,140.10},{"mizh-md5-48-2.cnf",SAT,152.91},{"mizh-md5-48-5.cnf",SAT,357.99},{"mizh-sha0-35-2.cnf",SAT,87.46},{"mizh-sha0-35-3.cnf",SAT,249.43},{"mizh-sha0-35-4.cnf",SAT,125.64},{"mizh-sha0-35-5.cnf",SAT,191.06},{"mizh-sha0-36-2.cnf",SAT,842.36},{"narain-vpn-clauses-6.cnf",UNK,3600.00},{"schup-l2s-guid-1-k56.cnf",UNS,774.69},{"schup-l2s-motst-2-k315.cnf",SAT,1427.20},{"simon-s02b-dp11u10.cnf",UNS,183.06},{"simon-s02b-k2f-gr-rcs-w8.cnf",UNK,3600.00},{"simon-s02b-r4b1k1.1.cnf",SAT,228.71},{"simon-s02-w08-18.cnf",SAT,446.95},{"simon-s03-fifo8-300.cnf",UNS,145.93},{"simon-s03-fifo8-400.cnf",UNS,691.95},{"vange-col-abb313GPIA-9-c.cnf",UNK,3600.00},{"vange-col-inithx.i.1-cn-54.cnf",SAT,86.57},{"velev-engi-uns-1.0-4nd.cnf",UNS,46.29},{"velev-engi-uns-1.0-5c1.cnf",UNS,4.94},{"velev-fvp-sat-3.0-b18.cnf",UNK,3600.00},{"velev-live-uns-2.0-ebuf.cnf",UNS,76.31},{"velev-npe-1.0-9dlx-b71.cnf",SAT,357.60},{"velev-pipe-o-uns-1.0-7.cnf",UNK,3600.00},{"velev-pipe-o-uns-1.1-6.cnf",UNK,3600.00},{"velev-pipe-sat-1.0-b10.cnf",UNK,3600.00},{"velev-pipe-sat-1.0-b7.cnf",UNK,3600.00},{"velev-pipe-sat-1.0-b9.cnf",SAT,37.58},{"velev-pipe-sat-1.1-b7.cnf",SAT,12.12},{"velev-pipe-uns-1.0-8.cnf",UNK,3600.00},{"velev-pipe-uns-1.0-9.cnf",UNK,3600.00},{"velev-pipe-uns-1.1-7.cnf",UNK,3600.00},{"velev-vliw-sat-2.0-b6.cnf",SAT,42.26},{"velev-vliw-sat-4.0-b1.cnf",SAT,203.44},{"velev-vliw-sat-4.0-b3.cnf",SAT,104.61},{"velev-vliw-sat-4.0-b4.cnf",SAT,100.46},{"velev-vliw-uns-2.0-iq4.cnf",UNK,3600.00},{"velev-vliw-uns-4.0-9C1.cnf",UNK,3600.00}}