{{"aloul-chnl11-13.cnf",UNK,3600.00},{"anbul-dated-5-15-u.cnf",UNS,453.02},{"anbul-part-10-13-s.cnf",UNK,3600.00},{"anbul-part-10-15-s.cnf",SAT,735.99},{"babic-dspam-vc1080.cnf",UNS,0.89},{"babic-dspam-vc949.cnf",UNS,0.80},{"babic-dspam-vc973.cnf",UNS,1.91},{"cmu-bmc-barrel6.cnf",UNS,2.51},{"cmu-bmc-longmult13.cnf",UNS,18.77},{"cmu-bmc-longmult15.cnf",UNS,29.88},{"een-pico-prop00-75.cnf",UNS,2.09},{"een-pico-prop05-75.cnf",UNS,18.51},{"een-tip-sat-nusmv-t5.B.cnf",SAT,1.19},{"een-tip-sat-texas-tp-5e.cnf",SAT,0.11},{"een-tip-sat-vis-eisen.cnf",SAT,0.39},{"fuhs-aprove-15.cnf",UNS,29.06},{"fuhs-aprove-16.cnf",UNS,434.85},{"goldb-heqc-alu4mul.cnf",UNS,265.06},{"goldb-heqc-dalumul.cnf",UNS,2130.91},{"goldb-heqc-frg1mul.cnf",UNK,3600.00},{"goldb-heqc-x1mul.cnf",UNK,3600.00},{"grieu-vmpc-27.cnf",SAT,8.22},{"grieu-vmpc-31.cnf",SAT,2005.52},{"hoons-vbmc-lucky7.cnf",UNS,0.86},{"ibm-2002-04r-k80.cnf",SAT,56.68},{"ibm-2002-11r1-k45.cnf",SAT,33.51},{"ibm-2002-18r-k90.cnf",SAT,67.92},{"ibm-2002-20r-k75.cnf",SAT,127.39},{"ibm-2002-22r-k60.cnf",UNS,255.20},{"ibm-2002-22r-k75.cnf",SAT,90.71},{"ibm-2002-22r-k80.cnf",SAT,198.97},{"ibm-2002-23r-k90.cnf",SAT,390.50},{"ibm-2002-24r3-k100.cnf",UNS,267.04},{"ibm-2002-25r-k10.cnf",UNS,1088.80},{"ibm-2002-29r-k75.cnf",SAT,89.26},{"ibm-2002-30r-k85.cnf",SAT,947.89},{"ibm-2002-31_1r3-k30.cnf",UNS,326.66},{"ibm-2004-01-k90.cnf",SAT,27.38},{"ibm-2004-1_11-k80.cnf",SAT,224.19},{"ibm-2004-23-k100.cnf",SAT,467.78},{"ibm-2004-23-k80.cnf",SAT,201.44},{"ibm-2004-29-k25.cnf",UNS,80.13},{"ibm-2004-29-k55.cnf",SAT,17.79},{"ibm-2004-3_02_3-k95.cnf",SAT,2.15},{"jarvi-eq-atree-9.cnf",UNS,72.70},{"manol-pipe-c10nid_i.cnf",UNS,843.76},{"manol-pipe-c10nidw.cnf",UNS,1137.21},{"manol-pipe-c6bidw_i.cnf",UNS,74.32},{"manol-pipe-c8nidw.cnf",UNS,407.84},{"manol-pipe-c9n_i.cnf",UNS,21.07},{"manol-pipe-f7nidw.cnf",UNS,1216.54},{"manol-pipe-f9b.cnf",UNS,421.18},{"manol-pipe-g10bid_i.cnf",UNS,653.33},{"manol-pipe-g10nid.cnf",UNS,135.46},{"manol-pipe-g8nidw.cnf",UNS,126.25},{"marijn-philips.cnf",UNS,463.03},{"maris-s03-gripper11.cnf",SAT,26.50},{"mizh-md5-47-3.cnf",SAT,141.85},{"mizh-md5-47-4.cnf",SAT,193.24},{"mizh-md5-47-5.cnf",SAT,58.31},{"mizh-md5-48-2.cnf",SAT,184.41},{"mizh-md5-48-5.cnf",SAT,193.08},{"mizh-sha0-35-3.cnf",SAT,22.13},{"mizh-sha0-35-4.cnf",SAT,21.45},{"mizh-sha0-36-1.cnf",SAT,2125.14},{"mizh-sha0-36-3.cnf",SAT,170.29},{"mizh-sha0-36-4.cnf",SAT,271.11},{"narain-vpn-clauses-10.cnf",UNS,90.88},{"narain-vpn-clauses-8.cnf",UNK,3600.00},{"palac-sn7-ipc5-h16.cnf",SAT,180.41},{"palac-uts-l06-ipc5-h34.cnf",SAT,39.90},{"post-c32s-col400-16.cnf",UNS,59.31},{"post-c32s-gcdm16-22.cnf",SAT,247.56},{"post-c32s-gcdm16-23.cnf",UNS,330.85},{"post-c32s-ss-8.cnf",UNS,2951.23},{"post-cbmc-aes-d-r1.cnf",UNS,3.64},{"post-cbmc-aes-d-r2.cnf",UNK,3600.00},{"post-cbmc-aes-ee-r2.cnf",UNK,3600.00},{"post-cbmc-aes-ee-r3.cnf",UNK,3600.00},{"post-cbmc-aes-ele.cnf",UNS,126.85},{"post-cbmc-zfcp-2.8-u2.cnf",UNK,3600.00},{"schup-l2s-abp4-1-k31.cnf",UNS,17.16},{"schup-l2s-bc56s-1-k391.cnf",UNS,1682.56},{"schup-l2s-motst-2-k315.cnf",SAT,36.58},{"simon-s02b-r4b1k1.1.cnf",SAT,323.65},{"simon-s02b-r4b1k1.2.cnf",SAT,39.35},{"simon-s02-f2clk-50.cnf",UNS,430.82},{"simon-s03-fifo8-400.cnf",UNS,82.63},{"simon-s03-w08-15.cnf",SAT,104.08},{"vange-col-abb313GPIA-9-c.cnf",UNK,3600.00},{"velev-engi-uns-1.0-4nd.cnf",UNS,15.90},{"velev-fvp-sat-3.0-b18.cnf",SAT,31.01},{"velev-npe-1.0-9dlx-b71.cnf",SAT,337.26},{"velev-vliw-sat-4.0-b4.cnf",SAT,30.86},{"velev-vliw-sat-4.0-b8.cnf",SAT,388.30},{"velev-vliw-uns-2.0-iq1.cnf",UNK,3600.00},{"velev-vliw-uns-2.0-iq2.cnf",UNK,3600.00},{"velev-vliw-uns-2.0-uq5.cnf",UNK,3600.00},{"velev-vliw-uns-4.0-9.cnf",UNK,3600.00},{"velev-vliw-uns-4.0-9-i1.cnf",UNK,3600.00}}