Siege v4<p>
22 groups, 251 instances, 2-hour cutoff<p>
Instances solved: 182 (67 SAT + 115 UNSAT)<br>
Time: 644109 seconds / 178.92 hours / 7.45 days<br>
Time on solved instances: 147309 seconds (36047 SAT + 111262 UNSAT)<p>
Instances solved in 10 minutes: 122 (13501 seconds)<br>
Instances solved in 15 minutes: 134 (21964 seconds)<br>
Instances solved in 20 minutes: 144 (32182 seconds)<br>
Instances solved in 30 minutes: 158 (53271 seconds)<br>
Instances solved in 60 minutes: 169 (80850 seconds)<br>
Instances solved in 90 minutes: 178 (120619 seconds)<br>
<p>Instances solved and time on solved instances by group:<p><table border=0>
<tr><td>dlx_iq_unsat_1.0</td><td width=20></td><td>17</td><td>/</td><td>32</td><td width=20></td><td>47642.726</td></tr>
<tr><td>engine_unsat_1.0</td><td width=20></td><td>7</td><td>/</td><td>10</td><td width=20></td><td>1967.49</td></tr>
<tr><td>fvp-sat.3.0</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>4480.364</td></tr>
<tr><td>fvp-unsat.1.0</td><td width=20></td><td>4</td><td>/</td><td>4</td><td width=20></td><td>19.545</td></tr>
<tr><td>fvp-unsat.2.0</td><td width=20></td><td>22</td><td>/</td><td>22</td><td width=20></td><td>258.254</td></tr>
<tr><td>fvp-unsat.3.0</td><td width=20></td><td>5</td><td>/</td><td>6</td><td width=20></td><td>7409.759</td></tr>
<tr><td>liveness_sat_1.0</td><td width=20></td><td>6</td><td>/</td><td>10</td><td width=20></td><td>4045.355</td></tr>
<tr><td>liveness_unsat_1.0</td><td width=20></td><td>4</td><td>/</td><td>12</td><td width=20></td><td>1716.474</td></tr>
<tr><td>liveness_unsat_2.0</td><td width=20></td><td>3</td><td>/</td><td>9</td><td width=20></td><td>46.969</td></tr>
<tr><td>npe-1.0</td><td width=20></td><td>3</td><td>/</td><td>6</td><td width=20></td><td>40.628</td></tr>
<tr><td>pipe_ooo_unsat_1.0</td><td width=20></td><td>8</td><td>/</td><td>15</td><td width=20></td><td>2073.673</td></tr>
<tr><td>pipe_ooo_unsat_1.1</td><td width=20></td><td>9</td><td>/</td><td>14</td><td width=20></td><td>2594.908</td></tr>
<tr><td>pipe_sat_1.0</td><td width=20></td><td>10</td><td>/</td><td>10</td><td width=20></td><td>5722.205</td></tr>
<tr><td>pipe_sat_1.1</td><td width=20></td><td>10</td><td>/</td><td>10</td><td width=20></td><td>4712.839</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>12</td><td>/</td><td>13</td><td width=20></td><td>8663.471</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>14</td><td>/</td><td>14</td><td width=20></td><td>10214.583</td></tr>
<tr><td>vliw_sat_2.0</td><td width=20></td><td>9</td><td>/</td><td>9</td><td width=20></td><td>10708.85</td></tr>
<tr><td>vliw_sat_2.1</td><td width=20></td><td>2</td><td>/</td><td>10</td><td width=20></td><td>5328.344</td></tr>
<tr><td>vliw_sat_4.0</td><td width=20></td><td>7</td><td>/</td><td>10</td><td width=20></td><td>1036.742</td></tr>
<tr><td>vliw_unsat_2.0</td><td width=20></td><td>7</td><td>/</td><td>9</td><td width=20></td><td>21025.483</td></tr>
<tr><td>vliw_unsat_3.0</td><td width=20></td><td>2</td><td>/</td><td>2</td><td width=20></td><td>6654.03</td></tr>
<tr><td>vliw_unsat_4.0</td><td width=20></td><td>1</td><td>/</td><td>4</td><td width=20></td><td>946.144</td></tr>
</table>
<p>

dlx_iq_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>143519</td><td>4852179</td><td>171415</td><td>612.144</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq34_a.cnf</td><td>154300</td><td>5176719</td><td>146497</td><td>603.504</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq35_a.cnf</td><td>165600</td><td>5831883</td><td>218996</td><td>971.188</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td><td>228994</td><td>6510624</td><td>204880</td><td>1546.86</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td><td>245646</td><td>7494625</td><td>201874</td><td>1774.56</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>202734</td><td>7166092</td><td>191241</td><td>1096.19</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>216230</td><td>6942168</td><td>230375</td><td>1439.18</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>230305</td><td>8237110</td><td>247604</td><td>1694.86</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td><td>244971</td><td>9200768</td><td>268358</td><td>1964.86</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq42_a.cnf</td><td>260240</td><td>10460400</td><td>301508</td><td>2294.61</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>276124</td><td>11223000</td><td>355733</td><td>3111.68</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td><td>292635</td><td>12368890</td><td>380864</td><td>3945.38</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td><td>309785</td><td>12943597</td><td>408719</td><td>4250.11</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td><td>327586</td><td>14441511</td><td>444092</td><td>4951.47</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td><td>346050</td><td>16363927</td><td>492517</td><td>5871.34</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td><td>365189</td><td>15266573</td><td>381472</td><td>4646.18</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td><td>385015</td><td>18320789</td><td>469184</td><td>6868.61</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td><td>405540</td></td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td><td>426776</td></td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td><td>448735</td></td></tr>
<tr><td>1dlx_c_iq53_a.cnf</td><td>471429</td></td></tr>
<tr><td>1dlx_c_iq54_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq55_a.cnf</td><td>519070</td></td></tr>
<tr><td>1dlx_c_iq56_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq57_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq58_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq59_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq60_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq61_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq62_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq63_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq64_a.cnf</td></td></tr>
<tr><td>Total (17 / 32)</td><td></td><td>172800855</td><td>5115329</td><td>47642.726</td><td></td></tr></table><p>
engine_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>engine_4.cnf</td><td>6944</td><td>57446</td><td>39081</td><td>9.812</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>7000</td><td>236112</td><td>183597</td><td>71.696</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td><td>18788</td><td>2041211</td><td>1634189</td><td>1405.3</td><td>UNSAT</td></tr>
<tr><td>engine_5_case1.cnf</td><td>18810</td><td>21680</td><td>13537</td><td>4.634</td><td>UNSAT</td></tr>
<tr><td>engine_5_nd.cnf</td><td>18878</td></td></tr>
<tr><td>engine_5_nd_case1.cnf</td><td>18900</td><td>61747</td><td>43618</td><td>18.154</td><td>UNSAT</td></tr>
<tr><td>engine_6.cnf</td><td>45276</td></td></tr>
<tr><td>engine_6_case1.cnf</td><td>45303</td><td>86530</td><td>59441</td><td>46.636</td><td>UNSAT</td></tr>
<tr><td>engine_6_nd.cnf</td><td>45408</td></td></tr>
<tr><td>engine_6_nd_case1.cnf</td><td>45435</td><td>405167</td><td>325886</td><td>411.258</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 10)</td><td></td><td>2909893</td><td>2299349</td><td>1967.49</td><td></td></tr></table><p>
fvp-sat.3.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>pipe_64_4_bug01.cnf</td><td>35853</td><td>489281</td><td>29254</td><td>10.976</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td><td>35853</td><td>3635208</td><td>805382</td><td>363.454</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>35947</td><td>193315</td><td>3467</td><td>3.756</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>35854</td><td>241547</td><td>5265</td><td>4.466</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug05.cnf</td><td>35853</td><td>5253770</td><td>1038256</td><td>567.55</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug06.cnf</td><td>35853</td><td>1636111</td><td>237489</td><td>87.745</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug07.cnf</td><td>35853</td><td>2891825</td><td>549281</td><td>236.43</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>35622</td><td>462994</td><td>34209</td><td>10.699</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>35726</td><td>500085</td><td>30114</td><td>11.498</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>35839</td><td>56383</td><td>599</td><td>0.466</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>35853</td><td>8563413</td><td>2025421</td><td>981.143</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>35854</td><td>485215</td><td>30528</td><td>11.304</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>35855</td><td>2706212</td><td>554260</td><td>210.408</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>35855</td><td>324643</td><td>10769</td><td>5.605</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td><td>35853</td><td>2973206</td><td>600002</td><td>227.457</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>35853</td><td>2847293</td><td>567901</td><td>230.332</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug17.cnf</td><td>35853</td><td>2820021</td><td>564232</td><td>223.282</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug18.cnf</td><td>35853</td><td>4484112</td><td>926516</td><td>434.79</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug19.cnf</td><td>35852</td><td>7767947</td><td>1589806</td><td>787.188</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug20.cnf</td><td>35853</td><td>1303705</td><td>224293</td><td>71.815</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td></td><td>49636286</td><td>9827044</td><td>4480.364</td><td></td></tr></table><p>
fvp-unsat.1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_mc_ex_bp_f.cnf</td><td>776</td><td>2745</td><td>688</td><td>0.017</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_mc_ex_bp_f.cnf</td><td>3250</td><td>24757</td><td>7337</td><td>0.523</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>4583</td><td>34185</td><td>7773</td><td>0.628</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>20093</td><td>730355</td><td>92984</td><td>18.377</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td></td><td>792042</td><td>108782</td><td>19.545</td><td></td></tr></table><p>
fvp-unsat.2.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>2pipe.cnf</td><td>892</td><td>4155</td><td>1741</td><td>0.056</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>834</td><td>4541</td><td>2423</td><td>0.096</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>925</td><td>4552</td><td>2269</td><td>0.086</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>2468</td><td>25197</td><td>8718</td><td>0.526</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>2223</td><td>16073</td><td>7620</td><td>0.486</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>2400</td><td>23858</td><td>9465</td><td>0.692</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2577</td><td>26745</td><td>11997</td><td>1.007</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>5237</td><td>98531</td><td>31725</td><td>4.03</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>4647</td><td>59881</td><td>27800</td><td>3.512</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>4941</td><td>70755</td><td>30660</td><td>4.147</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>5233</td><td>82797</td><td>33116</td><td>4.933</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>5525</td><td>90161</td><td>36656</td><td>5.528</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>9471</td><td>139115</td><td>15618</td><td>2.584</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>8441</td><td>146601</td><td>58115</td><td>13.545</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>8851</td><td>145892</td><td>55019</td><td>13.598</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>9267</td><td>133506</td><td>47582</td><td>12.06</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>9764</td><td>254647</td><td>90128</td><td>23.142</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>10113</td><td>150600</td><td>47137</td><td>12.471</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td><td>15800</td><td>518038</td><td>91997</td><td>28.77</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>17064</td><td>485418</td><td>146967</td><td>63.59</td><td>UNSAT</td></tr>
<tr><td>7pipe.cnf</td><td>23910</td><td>997777</td><td>131085</td><td>59.187</td><td>UNSAT</td></tr>
<tr><td>7pipe_bug.cnf</td><td>24065</td><td>282794</td><td>12309</td><td>4.208</td><td>SAT</td></tr>
<tr><td>Total (22 / 22)</td><td></td><td>3761634</td><td>900147</td><td>258.254</td><td></td></tr></table><p>
fvp-unsat.3.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>pipe_64_01.cnf</td><td>40347</td><td>4548034</td><td>609875</td><td>433.688</td><td>UNSAT</td></tr>
<tr><td>pipe_64_02.cnf</td><td>41774</td><td>6198018</td><td>808717</td><td>651.451</td><td>UNSAT</td></tr>
<tr><td>pipe_64_04.cnf</td><td>35853</td><td>9772721</td><td>2130223</td><td>1338.26</td><td>UNSAT</td></tr>
<tr><td>pipe_64_08.cnf</td><td>50879</td><td>10824741</td><td>1053928</td><td>1242.89</td><td>UNSAT</td></tr>
<tr><td>pipe_64_16.cnf</td><td>64262</td><td>24872095</td><td>2165498</td><td>3743.47</td><td>UNSAT</td></tr>
<tr><td>pipe_64_32.cnf</td><td>95179</td></td></tr>
<tr><td>Total (5 / 6)</td><td></td><td>56215609</td><td>6768241</td><td>7409.759</td><td></td></tr></table><p>
liveness_sat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug10_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug1_liveness.cnf</td><td>171648</td><td>358865</td><td>62140</td><td>255.274</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>196655</td><td>277728</td><td>39979</td><td>87.267</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>224920</td><td>470917</td><td>75454</td><td>397.118</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>256697</td><td>421476</td><td>69064</td><td>457.002</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug5_liveness.cnf</td><td>292249</td><td>968880</td><td>212299</td><td>2183.34</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td><td>331848</td><td>471764</td><td>77397</td><td>665.354</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug7_liveness.cnf</td><td>375775</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug8_liveness.cnf</td><td>424320</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug9_liveness.cnf</td><td>477782</td></td></tr>
<tr><td>Total (6 / 10)</td><td></td><td>2969630</td><td>536333</td><td>4045.355</td><td></td></tr></table><p>
liveness_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bp_f_liveness.cnf</td><td>9474</td><td>163132</td><td>86679</td><td>25.652</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td><td>24104</td><td>2580031</td><td>1662332</td><td>1666.31</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>18274</td><td>135170</td><td>64954</td><td>22.037</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>6128</td><td>46855</td><td>21645</td><td>2.475</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_bp_f_liveness.cnf</td><td>202253</td></td></tr>
<tr><td>2dlx_ca_ex_bp_f_liveness.cnf</td><td>421107</td></td></tr>
<tr><td>2dlx_ca_ex_liveness.cnf</td><td>318771</td></td></tr>
<tr><td>2dlx_ca_liveness.cnf</td><td>115049</td></td></tr>
<tr><td>2dlx_cc_bp_f_liveness.cnf</td><td>267364</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_liveness.cnf</td><td>352057</td></td></tr>
<tr><td>2dlx_cc_liveness.cnf</td><td>122395</td></td></tr>
<tr><td>Total (4 / 12)</td><td></td><td>2925188</td><td>1835610</td><td>1716.474</td><td></td></tr></table><p>
liveness_unsat_2.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bp_u_f_liveness.cnf</td><td>6874</td><td>54854</td><td>21928</td><td>2.846</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>14628</td><td>199604</td><td>90024</td><td>24.721</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>16011</td><td>144065</td><td>69166</td><td>19.402</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_bp_u_f_liveness.cnf</td><td>121388</td></td></tr>
<tr><td>2dlx_ca_ex_bp_u_f_liveness.cnf</td><td>223527</td></td></tr>
<tr><td>2dlx_ca_ex_d_liveness.cnf</td><td>235853</td></td></tr>
<tr><td>2dlx_cc_bp_u_f_liveness.cnf</td><td>144071</td></td></tr>
<tr><td>2dlx_cc_ex_bp_u_f_liveness.cnf</td><td>258649</td></td></tr>
<tr><td>2dlx_cc_ex_d_liveness.cnf</td><td>266476</td></td></tr>
<tr><td>Total (3 / 9)</td><td></td><td>398523</td><td>181118</td><td>46.969</td><td></td></tr></table><p>
npe-1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bug_no_pe.cnf</td><td>3295</td><td>22405</td><td>11638</td><td>0.932</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>3295</td><td>191223</td><td>139134</td><td>32.721</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf</td><td>96675</td><td>135850</td><td>8808</td><td>6.975</td><td>SAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_no_pe.cnf</td><td>96675</td></td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_no_pe.cnf</td></td></tr>
<tr><td>Total (3 / 6)</td><td></td><td>349478</td><td>159580</td><td>40.628</td><td></td></tr></table><p>
pipe_ooo_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>10pipe_10_ooo.cnf</td><td>67050</td></td></tr>
<tr><td>11pipe_11_ooo.cnf</td><td>88289</td></td></tr>
<tr><td>12pipe_12_ooo.cnf</td><td>113768</td></td></tr>
<tr><td>13pipe_13_ooo.cnf</td><td>143311</td></td></tr>
<tr><td>14pipe_14_ooo.cnf</td><td>179056</td></td></tr>
<tr><td>15pipe_15_ooo.cnf</td><td>219755</td></td></tr>
<tr><td>16pipe_16_ooo.cnf</td><td>266498</td></td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>918</td><td>4049</td><td>1954</td><td>0.064</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2533</td><td>28326</td><td>13999</td><td>1.28</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>5356</td><td>91162</td><td>36148</td><td>5.57</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>9705</td><td>175130</td><td>58102</td><td>14.689</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>15948</td><td>439365</td><td>141250</td><td>57.994</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo.cnf</td><td>24415</td><td>846342</td><td>239173</td><td>146.749</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo.cnf</td><td>35510</td><td>1910486</td><td>545192</td><td>499.787</td><td>UNSAT</td></tr>
<tr><td>9pipe_9_ooo.cnf</td><td>49309</td><td>3114913</td><td>1093078</td><td>1347.54</td><td>UNSAT</td></tr>
<tr><td>Total (8 / 15)</td><td></td><td>6609773</td><td>2128896</td><td>2073.673</td><td></td></tr></table><p>
pipe_ooo_unsat_1.1
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>10pipe_10_ooo_q0_T0.cnf</td><td>81932</td><td>10393415</td><td>1468394</td><td>1863.56</td><td>UNSAT</td></tr>
<tr><td>11pipe_11_ooo_q0_T0.cnf</td><td>110150</td></td></tr>
<tr><td>12pipe_12_ooo_q0_T0.cnf</td><td>144721</td></td></tr>
<tr><td>13pipe_13_ooo_q0_T0.cnf</td><td>185924</td></td></tr>
<tr><td>14pipe_14_ooo_q0_T0.cnf</td><td>236250</td></td></tr>
<tr><td>15pipe_15_ooo_q0_T0.cnf</td><td>294982</td></td></tr>
<tr><td>2pipe_2_ooo_q0_T0.cnf</td><td>895</td><td>5876</td><td>2551</td><td>0.077</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>2566</td><td>30752</td><td>11579</td><td>0.822</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>5605</td><td>92634</td><td>23778</td><td>2.712</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td><td>10482</td><td>255362</td><td>52015</td><td>9.778</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td><td>17710</td><td>577510</td><td>95396</td><td>30.176</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td><td>27846</td><td>1208946</td><td>183073</td><td>83.424</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td><td>41491</td><td>2387218</td><td>298706</td><td>192.171</td><td>UNSAT</td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td><td>59024</td><td>4152648</td><td>498533</td><td>412.188</td><td>UNSAT</td></tr>
<tr><td>Total (9 / 14)</td><td></td><td>19104361</td><td>2634025</td><td>2594.908</td><td></td></tr></table><p>
pipe_sat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug1.cnf</td><td>118040</td><td>2558527</td><td>199286</td><td>1169.92</td><td>SAT</td></tr>
<tr><td>12pipe_bug10.cnf</td><td>118040</td><td>1541525</td><td>100024</td><td>567.546</td><td>SAT</td></tr>
<tr><td>12pipe_bug2.cnf</td><td>118040</td><td>1317490</td><td>97951</td><td>551.754</td><td>SAT</td></tr>
<tr><td>12pipe_bug3.cnf</td><td>118039</td><td>690959</td><td>31914</td><td>71.879</td><td>SAT</td></tr>
<tr><td>12pipe_bug4.cnf</td><td>117504</td><td>974802</td><td>47678</td><td>294.366</td><td>SAT</td></tr>
<tr><td>12pipe_bug5.cnf</td><td>118040</td><td>2049901</td><td>166483</td><td>940.919</td><td>SAT</td></tr>
<tr><td>12pipe_bug6.cnf</td><td>117665</td><td>2644036</td><td>210732</td><td>1093.99</td><td>SAT</td></tr>
<tr><td>12pipe_bug7.cnf</td><td>118040</td><td>1496050</td><td>108318</td><td>581.158</td><td>SAT</td></tr>
<tr><td>12pipe_bug8.cnf</td><td>117526</td><td>312496</td><td>9244</td><td>23.204</td><td>SAT</td></tr>
<tr><td>12pipe_bug9.cnf</td><td>118038</td><td>1429081</td><td>88901</td><td>427.469</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td></td><td>15014867</td><td>1060531</td><td>5722.205</td><td></td></tr></table><p>
pipe_sat_1.1
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug10_q0.cnf</td><td>138918</td><td>4479121</td><td>324293</td><td>1030.66</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td><td>138917</td><td>3709521</td><td>271089</td><td>824.113</td><td>SAT</td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>138918</td><td>1551407</td><td>73627</td><td>215.93</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>138917</td><td>3332853</td><td>218780</td><td>698.488</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>138563</td><td>374267</td><td>12787</td><td>24.765</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>138918</td><td>2786968</td><td>181705</td><td>554.797</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>138795</td><td>796919</td><td>29111</td><td>68.848</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>138918</td><td>3219722</td><td>256155</td><td>725.778</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td><td>138711</td><td>258587</td><td>9354</td><td>18.477</td><td>SAT</td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>138916</td><td>2724037</td><td>191721</td><td>550.983</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td></td><td>23233402</td><td>1568622</td><td>4712.839</td><td></td></tr></table><p>
pipe_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_k.cnf</td><td>860</td><td>3743</td><td>1479</td><td>0.04</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>2391</td><td>20611</td><td>7290</td><td>0.422</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td><td>5095</td><td>92870</td><td>32472</td><td>3.877</td><td>UNSAT</td></tr>
<tr><td>05pipe_k.cnf</td><td>9330</td><td>267829</td><td>58036</td><td>11.408</td><td>UNSAT</td></tr>
<tr><td>06pipe_k.cnf</td><td>15346</td><td>333794</td><td>26238</td><td>6.768</td><td>UNSAT</td></tr>
<tr><td>07pipe_k.cnf</td><td>23909</td><td>1060754</td><td>111915</td><td>51.821</td><td>UNSAT</td></tr>
<tr><td>08pipe_k.cnf</td><td>35065</td><td>1929666</td><td>164514</td><td>118.754</td><td>UNSAT</td></tr>
<tr><td>09pipe_k.cnf</td><td>49112</td><td>2222244</td><td>89282</td><td>97.775</td><td>UNSAT</td></tr>
<tr><td>10pipe_k.cnf</td><td>67300</td><td>6125882</td><td>376789</td><td>681.387</td><td>UNSAT</td></tr>
<tr><td>11pipe_k.cnf</td><td>89315</td><td>9769169</td><td>469186</td><td>991.049</td><td>UNSAT</td></tr>
<tr><td>12pipe_k.cnf</td><td>115915</td><td>18475028</td><td>703504</td><td>2620.89</td><td>UNSAT</td></tr>
<tr><td>13pipe_k.cnf</td><td>147626</td><td>30023805</td><td>912664</td><td>4079.28</td><td>UNSAT</td></tr>
<tr><td>14pipe_k.cnf</td><td>184980</td></td></tr>
<tr><td>Total (12 / 13)</td><td></td><td>70325395</td><td>2953369</td><td>8663.471</td><td></td></tr></table><p>
pipe_unsat_1.1
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_q0_k.cnf</td><td>873</td><td>6207</td><td>3143</td><td>0.115</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>2476</td><td>21133</td><td>6569</td><td>0.345</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>5380</td><td>94251</td><td>27105</td><td>3.102</td><td>UNSAT</td></tr>
<tr><td>05pipe_q0_k.cnf</td><td>10026</td><td>241671</td><td>53416</td><td>9.275</td><td>UNSAT</td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>16775</td><td>333603</td><td>24941</td><td>5.631</td><td>UNSAT</td></tr>
<tr><td>07pipe_q0_k.cnf</td><td>26512</td><td>867932</td><td>99942</td><td>36.828</td><td>UNSAT</td></tr>
<tr><td>08pipe_q0_k.cnf</td><td>39434</td><td>1467045</td><td>141345</td><td>76.613</td><td>UNSAT</td></tr>
<tr><td>09pipe_q0_k.cnf</td><td>55996</td><td>2080807</td><td>84251</td><td>64.5</td><td>UNSAT</td></tr>
<tr><td>10pipe_q0_k.cnf</td><td>77639</td><td>4314904</td><td>257142</td><td>259.781</td><td>UNSAT</td></tr>
<tr><td>11pipe_q0_k.cnf</td><td>104244</td><td>6806361</td><td>328177</td><td>465.179</td><td>UNSAT</td></tr>
<tr><td>12pipe_q0_k.cnf</td><td>136800</td><td>11052415</td><td>415014</td><td>809.834</td><td>UNSAT</td></tr>
<tr><td>13pipe_q0_k.cnf</td><td>176066</td><td>15949996</td><td>532665</td><td>1443.74</td><td>UNSAT</td></tr>
<tr><td>14pipe_q0_k.cnf</td><td>222845</td><td>24778145</td><td>651458</td><td>2496.06</td><td>UNSAT</td></tr>
<tr><td>15pipe_q0_k.cnf</td><td>277976</td><td>33172469</td><td>877368</td><td>4543.58</td><td>UNSAT</td></tr>
<tr><td>Total (14 / 14)</td><td></td><td>101186939</td><td>3502536</td><td>10214.583</td><td></td></tr></table><p>
vliw_sat_2.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug1.cnf</td><td>236038</td><td>6960878</td><td>305412</td><td>1316.4</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug2.cnf</td><td>235928</td><td>287284</td><td>329</td><td>1.901</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug3.cnf</td><td>235402</td><td>9226060</td><td>501133</td><td>1992.19</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug4.cnf</td><td>235277</td><td>8086656</td><td>386167</td><td>1596.74</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug5.cnf</td><td>235923</td><td>10627677</td><td>631104</td><td>2398.39</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>235926</td><td>1870970</td><td>38921</td><td>94.977</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>173811</td><td>6419841</td><td>360206</td><td>996.786</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>229942</td><td>5596046</td><td>176282</td><td>787.326</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td><td>235184</td><td>8598485</td><td>399317</td><td>1524.14</td><td>SAT</td></tr>
<tr><td>Total (9 / 9)</td><td></td><td>57673897</td><td>2798871</td><td>10708.85</td><td></td></tr></table><p>
vliw_sat_2.1
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug1.cnf</td><td>410707</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug10.cnf</td><td>408558</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug2.cnf</td><td>409731</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug3.cnf</td><td>410219</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug4.cnf</td><td>409220</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug5.cnf</td><td>410693</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug6.cnf</td><td>410553</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug7.cnf</td><td>410729</td><td>3471163</td><td>24745</td><td>126.054</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug8.cnf</td><td>410560</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug9.cnf</td><td>449867</td><td>22321212</td><td>769578</td><td>5202.29</td><td>SAT</td></tr>
<tr><td>Total (2 / 10)</td><td></td><td>25792375</td><td>794323</td><td>5328.344</td><td></td></tr></table><p>
vliw_sat_4.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug1.cnf</td><td>521188</td><td>4138878</td><td>26364</td><td>154.523</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>521182</td></td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>521158</td><td>3185190</td><td>16616</td><td>102.062</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>521046</td><td>4460466</td><td>24509</td><td>153.75</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>520721</td><td>4092308</td><td>19896</td><td>132.979</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>520770</td></td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>521192</td><td>4138295</td><td>37005</td><td>199.822</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>521147</td><td>4008315</td><td>15148</td><td>103.387</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>521179</td></td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>521187</td><td>4475278</td><td>30692</td><td>190.219</td><td>SAT</td></tr>
<tr><td>Total (7 / 10)</td><td></td><td>28498730</td><td>170230</td><td>1036.742</td><td></td></tr></table><p>
vliw_unsat_2.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq1.cnf</td><td>24604</td><td>2595744</td><td>286732</td><td>68.259</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td><td>44095</td><td>8299050</td><td>506575</td><td>232.28</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td><td>69789</td><td>19298388</td><td>860190</td><td>616.284</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq4.cnf</td><td>106013</td><td>43145115</td><td>1503639</td><td>1751.87</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq5.cnf</td><td>151669</td><td>92390629</td><td>2307944</td><td>4407.28</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6.cnf</td><td>209724</td><td>137247728</td><td>2517245</td><td>6634.42</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq7.cnf</td><td>306095</td><td>175068110</td><td>2211251</td><td>7315.09</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8.cnf</td><td>371419</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq9.cnf</td><td>482093</td></td></tr>
<tr><td>Total (7 / 9)</td><td></td><td>478044764</td><td>10193576</td><td>21025.483</td><td></td></tr></table><p>
vliw_unsat_3.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24.cnf</td><td>132413</td><td>213543551</td><td>2149974</td><td>3599.38</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24_D.cnf</td><td>132156</td><td>181449436</td><td>1817665</td><td>3054.65</td><td>UNSAT</td></tr>
<tr><td>Total (2 / 2)</td><td></td><td>394992987</td><td>3967639</td><td>6654.03</td><td></td></tr></table><p>
vliw_unsat_4.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Decisions</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9vliw_m_9stages_C1.cnf</td><td>96177</td><td>7649121</td><td>916115</td><td>946.144</td><td>UNSAT</td></tr>
<tr><td>9vliw_m_9stages_iq1_C1.cnf</td><td>154309</td></td></tr>
<tr><td>9vliw_m_9stages_iq2_C1.cnf</td><td>230662</td></td></tr>
<tr><td>9vliw_m_9stages_iq3_C1.cnf</td><td>333336</td></td></tr>
<tr><td>Total (1 / 4)</td><td></td><td>7649121</td><td>916115</td><td>946.144</td><td></td></tr></table><p>