Chaff II<p>
22 groups, 251 instances, 2-hour cutoff<p>
Instances solved: 148 (61 SAT + 87 UNSAT)<br>
Time: 901295 seconds / 250.36 hours / 10.43 days<br>
Time on solved instances: 159695 seconds (68021 SAT + 91674 UNSAT)<p>
Instances solved in 10 minutes: 93 (10233 seconds)<br>
Instances solved in 15 minutes: 98 (14098 seconds)<br>
Instances solved in 20 minutes: 109 (25965 seconds)<br>
Instances solved in 30 minutes: 118 (39108 seconds)<br>
Instances solved in 60 minutes: 131 (71258 seconds)<br>
Instances solved in 90 minutes: 140 (111470 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>10</td><td>/</td><td>32</td><td width=20></td><td>41681.69</td></tr>
<tr><td>engine_unsat_1.0</td><td width=20></td><td>6</td><td>/</td><td>10</td><td width=20></td><td>2684.4728</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>11129.312604</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>39.176055</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>898.67382</td></tr>
<tr><td>fvp-unsat.3.0</td><td width=20></td><td>0</td><td>/</td><td>6</td><td width=20></td><td>0</td></tr>
<tr><td>liveness_sat_1.0</td><td width=20></td><td>4</td><td>/</td><td>10</td><td width=20></td><td>7450.923</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>3952.49425</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>105.474</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>5889.61017</td></tr>
<tr><td>pipe_ooo_unsat_1.0</td><td width=20></td><td>6</td><td>/</td><td>15</td><td width=20></td><td>2770.348831</td></tr>
<tr><td>pipe_ooo_unsat_1.1</td><td width=20></td><td>7</td><td>/</td><td>14</td><td width=20></td><td>3121.478241</td></tr>
<tr><td>pipe_sat_1.0</td><td width=20></td><td>9</td><td>/</td><td>10</td><td width=20></td><td>11055.00787</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>14453.971903</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>9</td><td>/</td><td>13</td><td width=20></td><td>6355.935083</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>9</td><td>/</td><td>14</td><td width=20></td><td>5094.993746</td></tr>
<tr><td>vliw_sat_2.0</td><td width=20></td><td>3</td><td>/</td><td>9</td><td width=20></td><td>7723.16275</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>1188.687</td></tr>
<tr><td>vliw_sat_4.0</td><td width=20></td><td>10</td><td>/</td><td>10</td><td width=20></td><td>9213.874</td></tr>
<tr><td>vliw_unsat_2.0</td><td width=20></td><td>4</td><td>/</td><td>9</td><td width=20></td><td>9922.406</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>12074.31</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>2888.9</td></tr>
</table>
<p>

dlx_iq_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_iq42_a.cnf</td><td>18132907</td><td>260240</td><td>3617585</td><td>350593</td><td>6065.23</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>19418125</td><td>276124</td><td>3861235</td><td>329499</td><td>6067.22</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>7515080</td><td>143519</td><td>1877765</td><td>204892</td><td>1869.31</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq53_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq54_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq55_a.cnf</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_iq34_a.cnf</td><td>8227629</td><td>154300</td><td>2034001</td><td>197749</td><td>2012.37</td><td>UNSAT</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>1dlx_c_iq35_a.cnf</td><td>8648384</td><td>165600</td><td>2198895</td><td>217719</td><td>2308.23</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td><td>14308414</td><td>228994</td><td>4194027</td><td>252613</td><td>5402.48</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>13057445</td><td>202734</td><td>2748125</td><td>279972</td><td>3747.17</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>14049119</td><td>216230</td><td>2950261</td><td>302697</td><td>4328.37</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>16021394</td><td>230305</td><td>3162370</td><td>309482</td><td>4697.69</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td><td>16474837</td><td>244971</td><td>3384721</td><td>326277</td><td>5183.62</td><td>UNSAT</td></tr>
<tr><td>Total (10 / 32)</td><td>135853334</td><td colspan=2></td><td>2771493</td><td>41681.69</td><td></td></tr></table><p>
engine_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>engine_4.cnf</td><td>77588</td><td>6944</td><td>66654</td><td>46697</td><td>28.9836</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>542186</td><td>7000</td><td>67586</td><td>399544</td><td>497.165</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td></td></tr>
<tr><td>engine_5_case1.cnf</td><td>20331</td><td>18810</td><td>214185</td><td>12313</td><td>11.2213</td><td>UNSAT</td></tr>
<tr><td>engine_5_nd.cnf</td></td></tr>
<tr><td>engine_5_nd_case1.cnf</td><td>71875</td><td>18900</td><td>216246</td><td>48224</td><td>59.9399</td><td>UNSAT</td></tr>
<tr><td>engine_6.cnf</td></td></tr>
<tr><td>engine_6_case1.cnf</td><td>93517</td><td>45303</td><td>606068</td><td>56458</td><td>117.273</td><td>UNSAT</td></tr>
<tr><td>engine_6_nd.cnf</td></td></tr>
<tr><td>engine_6_nd_case1.cnf</td><td>824801</td><td>45435</td><td>610120</td><td>580998</td><td>1969.89</td><td>UNSAT</td></tr>
<tr><td>Total (6 / 10)</td><td>1630298</td><td colspan=2></td><td>1144234</td><td>2684.4728</td><td></td></tr></table><p>
fvp-sat.3.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>pipe_64_4_bug01.cnf</td><td>543914</td><td>35853</td><td>1012270</td><td>9233</td><td>25.9811</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td><td>32155371</td><td>35853</td><td>1012271</td><td>524177</td><td>3712.27</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>195530</td><td>35947</td><td>992674</td><td>2758</td><td>12.3121</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>361249</td><td>35854</td><td>1012315</td><td>6210</td><td>25.5181</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug05.cnf</td><td>20733142</td><td>35853</td><td>1012271</td><td>349092</td><td>2130.54</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug06.cnf</td><td>2571842</td><td>35853</td><td>1012271</td><td>46989</td><td>151.31</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug07.cnf</td><td>7399281</td><td>35853</td><td>1012271</td><td>132483</td><td>537.31</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>35461</td><td>35622</td><td>1003074</td><td>159</td><td>0.368944</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>504647</td><td>35726</td><td>1011764</td><td>8576</td><td>29.0826</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>1069488</td><td>35839</td><td>1012135</td><td>21866</td><td>42.0686</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>12603139</td><td>35853</td><td>1012271</td><td>220811</td><td>1111.31</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>521994</td><td>35854</td><td>1012275</td><td>10541</td><td>25.2882</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>804105</td><td>35855</td><td>1012302</td><td>17357</td><td>45.866</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>25504</td><td>35855</td><td>1012407</td><td>146</td><td>0.26196</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td><td>4945102</td><td>35853</td><td>1012271</td><td>100491</td><td>331.642</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>13903647</td><td>35853</td><td>1012271</td><td>257851</td><td>1280.09</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug17.cnf</td><td>4344241</td><td>35853</td><td>1012271</td><td>84065</td><td>300.898</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug18.cnf</td><td>8815380</td><td>35853</td><td>1012271</td><td>173545</td><td>705.941</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug19.cnf</td><td>5419304</td><td>35852</td><td>1012266</td><td>97313</td><td>358.778</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug20.cnf</td><td>4653511</td><td>35853</td><td>1012271</td><td>85223</td><td>302.476</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>121605852</td><td colspan=2></td><td>2148886</td><td>11129.312604</td><td></td></tr></table><p>
fvp-unsat.1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_mc_ex_bp_f.cnf</td><td>2464</td><td>776</td><td>3725</td><td>669</td><td>0.026996</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_mc_ex_bp_f.cnf</td><td>21148</td><td>3250</td><td>24640</td><td>5552</td><td>0.791879</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>31086</td><td>4583</td><td>41704</td><td>7531</td><td>1.42378</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>704080</td><td>20093</td><td>179492</td><td>48339</td><td>36.9334</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td>758778</td><td colspan=2></td><td>62091</td><td>39.176055</td><td></td></tr></table><p>
fvp-unsat.2.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>2pipe.cnf</td><td>2909</td><td>892</td><td>6695</td><td>1002</td><td>0.040994</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>2587</td><td>834</td><td>7026</td><td>1041</td><td>0.046993</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>3386</td><td>925</td><td>8213</td><td>1323</td><td>0.069989</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>18828</td><td>2468</td><td>27533</td><td>6068</td><td>0.817875</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>11851</td><td>2223</td><td>26561</td><td>4703</td><td>0.622905</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>17111</td><td>2400</td><td>29981</td><td>6202</td><td>0.962854</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>26757</td><td>2577</td><td>33270</td><td>9808</td><td>1.88671</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>104096</td><td>5237</td><td>80213</td><td>22720</td><td>9.44557</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>80562</td><td>4647</td><td>74554</td><td>18805</td><td>7.05293</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>114599</td><td>4941</td><td>82207</td><td>26124</td><td>11.3493</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>132985</td><td>5233</td><td>89473</td><td>18184</td><td>10.4314</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>126716</td><td>5525</td><td>96480</td><td>19842</td><td>11.7872</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>239887</td><td>9471</td><td>195452</td><td>15684</td><td>13.359</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>198285</td><td>8441</td><td>187545</td><td>32689</td><td>26.7749</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>211784</td><td>8851</td><td>201796</td><td>28907</td><td>27.7708</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>218436</td><td>9267</td><td>215440</td><td>26024</td><td>28.4557</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>402421</td><td>9764</td><td>221405</td><td>47554</td><td>56.7674</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>233985</td><td>10113</td><td>240892</td><td>25951</td><td>32.4281</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td><td>848090</td><td>15800</td><td>394739</td><td>56132</td><td>89.3014</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>812784</td><td>17064</td><td>545612</td><td>59420</td><td>164.938</td><td>UNSAT</td></tr>
<tr><td>7pipe.cnf</td><td>1815935</td><td>23910</td><td>751118</td><td>160184</td><td>396.475</td><td>UNSAT</td></tr>
<tr><td>7pipe_bug.cnf</td><td>129171</td><td>24065</td><td>731850</td><td>2872</td><td>7.8888</td><td>SAT</td></tr>
<tr><td>Total (22 / 22)</td><td>5753165</td><td colspan=2></td><td>591239</td><td>898.67382</td><td></td></tr></table><p>
fvp-unsat.3.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>pipe_64_01.cnf</td></td></tr>
<tr><td>pipe_64_02.cnf</td></td></tr>
<tr><td>pipe_64_04.cnf</td></td></tr>
<tr><td>pipe_64_08.cnf</td></td></tr>
<tr><td>pipe_64_16.cnf</td></td></tr>
<tr><td>pipe_64_32.cnf</td></td></tr>
<tr><td>Total (0 / 6)</td><td></td><td colspan=2></td><td></td><td>0</td><td></td></tr></table><p>
liveness_sat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</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>454827</td><td>171648</td><td>2614464</td><td>54177</td><td>461.333</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>406897</td><td>224920</td><td>3596474</td><td>17703</td><td>360.34</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>608775</td><td>256697</td><td>4205986</td><td>78640</td><td>1005.16</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug5_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td><td>1996247</td><td>331848</td><td>5706594</td><td>412402</td><td>5624.09</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug7_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug8_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug9_liveness.cnf</td></td></tr>
<tr><td>Total (4 / 10)</td><td>3466746</td><td colspan=2></td><td>562922</td><td>7450.923</td><td></td></tr></table><p>
liveness_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bp_f_liveness.cnf</td><td>322519</td><td>9474</td><td>107213</td><td>143489</td><td>127.298</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td><td>3152196</td><td>24104</td><td>339857</td><td>1252131</td><td>3767.47</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>160516</td><td>18274</td><td>202528</td><td>48817</td><td>50.1634</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>53120</td><td>6128</td><td>65112</td><td>22095</td><td>7.56285</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_ex_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_ex_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_liveness.cnf</td></td></tr>
<tr><td>Total (4 / 12)</td><td>3688351</td><td colspan=2></td><td>1466532</td><td>3952.49425</td><td></td></tr></table><p>
liveness_unsat_2.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bp_u_f_liveness.cnf</td><td>59145</td><td>6874</td><td>65479</td><td>17340</td><td>7.2499</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>194657</td><td>14628</td><td>161477</td><td>65045</td><td>59.304</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>136959</td><td>16011</td><td>210685</td><td>42818</td><td>38.9201</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_bp_u_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_ex_bp_u_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_ex_d_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_bp_u_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_u_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_d_liveness.cnf</td></td></tr>
<tr><td>Total (3 / 9)</td><td>390761</td><td colspan=2></td><td>125203</td><td>105.474</td><td></td></tr></table><p>
npe-1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bug_no_pe.cnf</td><td>46974</td><td>3295</td><td>35409</td><td>19470</td><td>6.11007</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>297446</td><td>3295</td><td>35410</td><td>138085</td><td>91.5201</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf</td></td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_no_pe.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf</td><td>2338183</td><td>889302</td><td>14582074</td><td>168409</td><td>5791.98</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_no_pe.cnf</td></td></tr>
<tr><td>Total (3 / 6)</td><td>2682603</td><td colspan=2></td><td>325964</td><td>5889.61017</td><td></td></tr></table><p>
pipe_ooo_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>10pipe_10_ooo.cnf</td></td></tr>
<tr><td>11pipe_11_ooo.cnf</td></td></tr>
<tr><td>12pipe_12_ooo.cnf</td></td></tr>
<tr><td>13pipe_13_ooo.cnf</td></td></tr>
<tr><td>14pipe_14_ooo.cnf</td></td></tr>
<tr><td>15pipe_15_ooo.cnf</td></td></tr>
<tr><td>16pipe_16_ooo.cnf</td><td>606656</td><td>266498</td><td>19470237</td><td>19261</td><td>639.619</td> (MEM OUT)</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>2427</td><td>918</td><td>8109</td><td>1168</td><td>0.058991</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>22791</td><td>2533</td><td>32182</td><td>9940</td><td>1.70474</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>134164</td><td>5356</td><td>89506</td><td>31479</td><td>14.7958</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>528258</td><td>9705</td><td>200959</td><td>100537</td><td>96.6393</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>1810015</td><td>15948</td><td>397032</td><td>269264</td><td>474.06</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo.cnf</td><td>5176939</td><td>24415</td><td>711050</td><td>765440</td><td>2183.09</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo.cnf</td></td></tr>
<tr><td>9pipe_9_ooo.cnf</td></td></tr>
<tr><td>Total (6 / 15)</td><td>8281250</td><td colspan=2></td><td>1197089</td><td>2770.348831</td><td></td></tr></table><p>
pipe_ooo_unsat_1.1
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>10pipe_10_ooo_q0_T0.cnf</td></td></tr>
<tr><td>11pipe_11_ooo_q0_T0.cnf</td></td></tr>
<tr><td>12pipe_12_ooo_q0_T0.cnf</td></td></tr>
<tr><td>13pipe_13_ooo_q0_T0.cnf</td></td></tr>
<tr><td>14pipe_14_ooo_q0_T0.cnf</td></td></tr>
<tr><td>15pipe_15_ooo_q0_T0.cnf</td></td></tr>
<tr><td>2pipe_2_ooo_q0_T0.cnf</td><td>3446</td><td>895</td><td>6561</td><td>1451</td><td>0.063991</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>24284</td><td>2566</td><td>25625</td><td>8697</td><td>1.20282</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>110845</td><td>5605</td><td>70042</td><td>31036</td><td>9.69553</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td><td>354904</td><td>10482</td><td>156027</td><td>47416</td><td>33.5879</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td><td>978998</td><td>17710</td><td>304026</td><td>99900</td><td>123.562</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td><td>2732555</td><td>27846</td><td>538853</td><td>272835</td><td>497.096</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td></td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td><td>9502608</td><td>59024</td><td>1430330</td><td>614926</td><td>2456.27</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 14)</td><td>13707640</td><td colspan=2></td><td>1076261</td><td>3121.478241</td><td></td></tr></table><p>
pipe_sat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug1.cnf</td><td>2927112</td><td>118040</td><td>8804672</td><td>63270</td><td>3112.93</td><td>SAT</td></tr>
<tr><td>12pipe_bug10.cnf</td><td>862310</td><td>118040</td><td>8804672</td><td>90505</td><td>1342.45</td><td>SAT</td></tr>
<tr><td>12pipe_bug2.cnf</td></td></tr>
<tr><td>12pipe_bug3.cnf</td><td>1341902</td><td>118039</td><td>8804669</td><td>37353</td><td>1185.43</td><td>SAT</td></tr>
<tr><td>12pipe_bug4.cnf</td><td>775977</td><td>117504</td><td>8743027</td><td>15011</td><td>542.288</td><td>SAT</td></tr>
<tr><td>12pipe_bug5.cnf</td><td>1949266</td><td>118040</td><td>8804672</td><td>38809</td><td>1779.74</td><td>SAT</td></tr>
<tr><td>12pipe_bug6.cnf</td><td>5564</td><td>117665</td><td>8647068</td><td>0</td><td>0.85987</td><td>SAT</td></tr>
<tr><td>12pipe_bug7.cnf</td><td>1697370</td><td>118040</td><td>8804672</td><td>55441</td><td>1775.69</td><td>SAT</td></tr>
<tr><td>12pipe_bug8.cnf</td><td>359380</td><td>117526</td><td>8760516</td><td>7214</td><td>253.52</td><td>SAT</td></tr>
<tr><td>12pipe_bug9.cnf</td><td>1213394</td><td>118038</td><td>8780591</td><td>25685</td><td>1062.1</td><td>SAT</td></tr>
<tr><td>Total (9 / 10)</td><td>11132275</td><td colspan=2></td><td>333288</td><td>11055.00787</td><td></td></tr></table><p>
pipe_sat_1.1
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug10_q0.cnf</td><td>2321307</td><td>138918</td><td>4678760</td><td>57927</td><td>1502.68</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td><td>1828250</td><td>138917</td><td>4678756</td><td>47103</td><td>1195.39</td><td>SAT</td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>2323797</td><td>138918</td><td>4678718</td><td>60677</td><td>1538.06</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>1956588</td><td>138917</td><td>4678757</td><td>50375</td><td>1347.95</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>1491789</td><td>138563</td><td>4675040</td><td>35936</td><td>930.841</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>6061046</td><td>138918</td><td>4678760</td><td>159182</td><td>5379.63</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>8658</td><td>138795</td><td>4671352</td><td>24</td><td>0.637903</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>1995669</td><td>138918</td><td>4678760</td><td>52957</td><td>1331.2</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td><td>387460</td><td>138711</td><td>4688614</td><td>7044</td><td>158.753</td><td>SAT</td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>1713548</td><td>138916</td><td>4676007</td><td>42833</td><td>1068.83</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td>20088112</td><td colspan=2></td><td>514058</td><td>14453.971903</td><td></td></tr></table><p>
pipe_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_k.cnf</td><td>2643</td><td>860</td><td>6693</td><td>1052</td><td>0.041994</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>20594</td><td>2391</td><td>27405</td><td>6662</td><td>0.927859</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td><td>95625</td><td>5095</td><td>79489</td><td>15738</td><td>5.74813</td><td>UNSAT</td></tr>
<tr><td>05pipe_k.cnf</td><td>388621</td><td>9330</td><td>189109</td><td>39047</td><td>32.716</td><td>UNSAT</td></tr>
<tr><td>06pipe_k.cnf</td><td>545500</td><td>15346</td><td>408792</td><td>24677</td><td>45.3271</td><td>UNSAT</td></tr>
<tr><td>07pipe_k.cnf</td><td>1725153</td><td>23909</td><td>751116</td><td>119290</td><td>296.837</td><td>UNSAT</td></tr>
<tr><td>08pipe_k.cnf</td><td>3329632</td><td>35065</td><td>1332773</td><td>221768</td><td>819.937</td><td>UNSAT</td></tr>
<tr><td>09pipe_k.cnf</td><td>6105914</td><td>49112</td><td>2317839</td><td>96507</td><td>1102.09</td><td>UNSAT</td></tr>
<tr><td>10pipe_k.cnf</td><td>10764206</td><td>67300</td><td>3601247</td><td>462609</td><td>4052.31</td><td>UNSAT</td></tr>
<tr><td>11pipe_k.cnf</td></td></tr>
<tr><td>12pipe_k.cnf</td></td></tr>
<tr><td>13pipe_k.cnf</td></td></tr>
<tr><td>14pipe_k.cnf</td></td></tr>
<tr><td>Total (9 / 13)</td><td>22977888</td><td colspan=2></td><td>987350</td><td>6355.935083</td><td></td></tr></table><p>
pipe_unsat_1.1
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_q0_k.cnf</td><td>3476</td><td>873</td><td>6457</td><td>1380</td><td>0.055992</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>21341</td><td>2476</td><td>25181</td><td>6918</td><td>0.758884</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>74840</td><td>5380</td><td>69072</td><td>21114</td><td>5.43017</td><td>UNSAT</td></tr>
<tr><td>05pipe_q0_k.cnf</td><td>248277</td><td>10026</td><td>154409</td><td>32148</td><td>19.0421</td><td>UNSAT</td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>396678</td><td>16775</td><td>315960</td><td>26197</td><td>29.1726</td><td>UNSAT</td></tr>
<tr><td>07pipe_q0_k.cnf</td><td>1737990</td><td>26512</td><td>536414</td><td>84788</td><td>200.316</td><td>UNSAT</td></tr>
<tr><td>08pipe_q0_k.cnf</td><td>4153813</td><td>39434</td><td>887706</td><td>157503</td><td>559.569</td><td>UNSAT</td></tr>
<tr><td>09pipe_q0_k.cnf</td><td>5428146</td><td>55996</td><td>1468197</td><td>98156</td><td>733.549</td><td>UNSAT</td></tr>
<tr><td>10pipe_q0_k.cnf</td><td>19063787</td><td>77639</td><td>2082017</td><td>318196</td><td>3547.1</td><td>UNSAT</td></tr>
<tr><td>11pipe_q0_k.cnf</td></td></tr>
<tr><td>12pipe_q0_k.cnf</td></td></tr>
<tr><td>13pipe_q0_k.cnf</td></td></tr>
<tr><td>14pipe_q0_k.cnf</td></td></tr>
<tr><td>15pipe_q0_k.cnf</td></td></tr>
<tr><td>Total (9 / 14)</td><td>31128348</td><td colspan=2></td><td>746400</td><td>5094.993746</td><td></td></tr></table><p>
vliw_sat_2.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug1.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug2.cnf</td><td>111987</td><td>235928</td><td>8076545</td><td>25</td><td>1.62575</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug3.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug4.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug5.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>4909986</td><td>235926</td><td>8076539</td><td>37270</td><td>522.387</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>20521810</td><td>229942</td><td>7882655</td><td>462872</td><td>7199.15</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td></td></tr>
<tr><td>Total (3 / 9)</td><td>25543783</td><td colspan=2></td><td>500167</td><td>7723.16275</td><td></td></tr></table><p>
vliw_sat_2.1
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug1.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug10.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug2.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug3.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug4.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug5.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug6.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug7.cnf</td><td>2177798</td><td>410729</td><td>15606974</td><td>3570</td><td>137.157</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug8.cnf</td><td>9352124</td><td>410560</td><td>15603495</td><td>49449</td><td>1051.53</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug9.cnf</td></td></tr>
<tr><td>Total (2 / 10)</td><td>11529922</td><td colspan=2></td><td>53019</td><td>1188.687</td><td></td></tr></table><p>
vliw_sat_4.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug1.cnf</td><td>11885940</td><td>521188</td><td>13378641</td><td>45314</td><td>2130.98</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>5293093</td><td>521182</td><td>13378625</td><td>20281</td><td>855.432</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>3047394</td><td>521158</td><td>13378532</td><td>8247</td><td>268.546</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>2011856</td><td>521046</td><td>13376161</td><td>5893</td><td>197.553</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>6823280</td><td>520721</td><td>13348117</td><td>27366</td><td>1245.13</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>15500798</td><td>520770</td><td>13380350</td><td>47935</td><td>2242.21</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>2730757</td><td>521192</td><td>13378781</td><td>8344</td><td>288.556</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>1640010</td><td>521147</td><td>13378010</td><td>4365</td><td>122.512</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>5749012</td><td>521179</td><td>13378617</td><td>25195</td><td>1112.52</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>5903203</td><td>521187</td><td>13378624</td><td>19657</td><td>750.435</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td>60585343</td><td colspan=2></td><td>212597</td><td>9213.874</td><td></td></tr></table><p>
vliw_unsat_2.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq1.cnf</td><td>3314109</td><td>24604</td><td>261473</td><td>261592</td><td>238.606</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td><td>11233921</td><td>44095</td><td>542253</td><td>547435</td><td>1041.5</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td><td>29680037</td><td>69789</td><td>968295</td><td>931399</td><td>3298.12</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq4.cnf</td><td>47564176</td><td>106013</td><td>1598301</td><td>961274</td><td>5344.18</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq5.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq7.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq9.cnf</td></td></tr>
<tr><td>Total (4 / 9)</td><td>91792243</td><td colspan=2></td><td>2701700</td><td>9922.406</td><td></td></tr></table><p>
vliw_unsat_3.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24.cnf</td><td>168686369</td><td>132413</td><td>1435600</td><td>1064493</td><td>6450.49</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24_D.cnf</td><td>154246734</td><td>132156</td><td>1434887</td><td>939805</td><td>5623.82</td><td>UNSAT</td></tr>
<tr><td>Total (2 / 2)</td><td>322933103</td><td colspan=2></td><td>2004298</td><td>12074.31</td><td></td></tr></table><p>
vliw_unsat_4.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Vars</td><td>Clauses</td><td>Conflicts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9vliw_m_9stages_C1.cnf</td><td>13026232</td><td>96177</td><td>1814189</td><td>703134</td><td>2888.9</td><td>UNSAT</td></tr>
<tr><td>9vliw_m_9stages_iq1_C1.cnf</td></td></tr>
<tr><td>9vliw_m_9stages_iq2_C1.cnf</td></td></tr>
<tr><td>9vliw_m_9stages_iq3_C1.cnf</td></td></tr>
<tr><td>Total (1 / 4)</td><td>13026232</td><td colspan=2></td><td>703134</td><td>2888.9</td><td></td></tr></table><p>