BerkMin<p>
22 groups, 251 instances, 1-hour cutoff<p>
Instances solved: 161 (58 SAT + 103 UNSAT)<br>
Time: 433588 seconds / 120.44 hours / 5.02 days<br>
Time on solved instances: 109588 seconds (50405 SAT + 59183 UNSAT)<p>
Instances solved in 10 minutes: 99 (8567 seconds)<br>
Instances solved in 15 minutes: 115 (20409 seconds)<br>
Instances solved in 20 minutes: 121 (26886 seconds)<br>
Instances solved in 30 minutes: 139 (53532 seconds)<br>
Instances solved in 60 minutes: 161 (109588 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>21</td><td>/</td><td>32</td><td width=20></td><td>31420.88</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>1177.65</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>12673.21</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>41.68</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>437.57</td></tr>
<tr><td>fvp-unsat.3.0</td><td width=20></td><td>1</td><td>/</td><td>6</td><td width=20></td><td>2790.7</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>4469.99</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>831.14</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>48.94</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>212.38</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>6230.63</td></tr>
<tr><td>pipe_ooo_unsat_1.1</td><td width=20></td><td>8</td><td>/</td><td>14</td><td width=20></td><td>1831.23</td></tr>
<tr><td>pipe_sat_1.0</td><td width=20></td><td>5</td><td>/</td><td>10</td><td width=20></td><td>1154.69</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>5565.12</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>3690.14</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>11</td><td>/</td><td>14</td><td width=20></td><td>4995.27</td></tr>
<tr><td>vliw_sat_2.0</td><td width=20></td><td>5</td><td>/</td><td>9</td><td width=20></td><td>7149.56</td></tr>
<tr><td>vliw_sat_2.1</td><td width=20></td><td>1</td><td>/</td><td>10</td><td width=20></td><td>622.01</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>18517.35</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>4898.09</td></tr>
<tr><td>vliw_unsat_3.0</td><td width=20></td><td>0</td><td>/</td><td>2</td><td width=20></td><td>0</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>829.6</td></tr>
</table>
<p>

dlx_iq_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_iq42_a.cnf</td><td>7195972</td><td>177995</td><td>8</td><td>1104.480</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>7153579</td><td>174671</td><td>8</td><td>1154.910</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td><td>7233951</td><td>167421</td><td>7</td><td>1260.680</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td><td>7945334</td><td>192929</td><td>8</td><td>1391.840</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td><td>9530159</td><td>196249</td><td>7</td><td>1719.770</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td><td>9923102</td><td>195467</td><td>8</td><td>1740.620</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td><td>10659628</td><td>198425</td><td>8</td><td>1889.040</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td><td>11441420</td><td>213200</td><td>8</td><td>2324.150</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td><td>12528536</td><td>226463</td><td>9</td><td>2374.970</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td><td>13759934</td><td>247024</td><td>9</td><td>2711.940</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>2768772</td><td>97161</td><td>8</td><td>329.270</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td><td>16340791</td><td>234185</td><td>8</td><td>2971.580</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq53_a.cnf</td><td>15548547</td><td>281220</td><td>9</td><td>3304.410</td><td>UNSAT</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>3004827</td><td>104871</td><td>8</td><td>364.520</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>3794205</td><td>113208</td><td>8</td><td>470.910</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td><td>7673204</td><td>118146</td><td>7</td><td>1394.250</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td><td>9415222</td><td>131298</td><td>7</td><td>1774.050</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>4632216</td><td>131464</td><td>8</td><td>634.630</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>5281767</td><td>138791</td><td>7</td><td>734.600</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>5919575</td><td>152494</td><td>7</td><td>852.590</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td><td>6199943</td><td>151638</td><td>7</td><td>917.670</td><td>UNSAT</td></tr>
<tr><td>Total (21 / 32)</td><td>177950684</td><td>3644320</td><td>164</td><td>31420.88</td><td></td></tr></table><p>
engine_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>engine_4.cnf</td><td>56269</td><td>36436</td><td>39</td><td>7.920</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>199145</td><td>146628</td><td>144</td><td>40.950</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td><td>1007017</td><td>771381</td><td>235</td><td>601.520</td><td>UNSAT</td></tr>
<tr><td>engine_5_case1.cnf</td><td>29843</td><td>22771</td><td>11</td><td>8.970</td><td>UNSAT</td></tr>
<tr><td>engine_5_nd.cnf</td></td></tr>
<tr><td>engine_5_nd_case1.cnf</td><td>72735</td><td>56094</td><td>20</td><td>23.040</td><td>UNSAT</td></tr>
<tr><td>engine_6.cnf</td></td></tr>
<tr><td>engine_6_case1.cnf</td><td>86029</td><td>68151</td><td>11</td><td>54.020</td><td>UNSAT</td></tr>
<tr><td>engine_6_nd.cnf</td></td></tr>
<tr><td>engine_6_nd_case1.cnf</td><td>493078</td><td>419390</td><td>49</td><td>441.230</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 10)</td><td>1944116</td><td>1520851</td><td>509</td><td>1177.65</td><td></td></tr></table><p>
fvp-sat.3.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>pipe_64_4_bug01.cnf</td><td>280696</td><td>19247</td><td>2</td><td>31.430</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td><td>9717796</td><td>1277977</td><td>81</td><td>2111.290</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>12035</td><td>725</td><td>1</td><td>3.110</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>39744</td><td>1604</td><td>1</td><td>9.370</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug05.cnf</td><td>5785416</td><td>760879</td><td>49</td><td>1226.870</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug06.cnf</td><td>5895955</td><td>846931</td><td>54</td><td>1109.400</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug07.cnf</td><td>6382440</td><td>909116</td><td>58</td><td>1297.580</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>344637</td><td>19387</td><td>2</td><td>39.780</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>577519</td><td>45707</td><td>3</td><td>60.140</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>146498</td><td>7512</td><td>1</td><td>20.130</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>2548599</td><td>340231</td><td>22</td><td>399.120</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>639859</td><td>46114</td><td>3</td><td>67.270</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>1401904</td><td>128954</td><td>9</td><td>149.610</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>397402</td><td>20163</td><td>2</td><td>44.350</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td><td>9797068</td><td>1334830</td><td>85</td><td>2104.750</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>4064510</td><td>498580</td><td>32</td><td>766.370</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug17.cnf</td><td>5961992</td><td>814923</td><td>52</td><td>1235.750</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug18.cnf</td><td>5156486</td><td>639605</td><td>41</td><td>811.670</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug19.cnf</td><td>2708035</td><td>346465</td><td>22</td><td>393.980</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug20.cnf</td><td>4767987</td><td>639024</td><td>41</td><td>791.240</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>66626578</td><td>8697974</td><td>561</td><td>12673.21</td><td></td></tr></table><p>
fvp-unsat.1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_mc_ex_bp_f.cnf</td><td>2251</td><td>618</td><td>6</td><td>0.010</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_mc_ex_bp_f.cnf</td><td>24863</td><td>4378</td><td>12</td><td>0.320</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>40633</td><td>11178</td><td>22</td><td>1.050</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>2106153</td><td>78267</td><td>30</td><td>40.300</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td>2173900</td><td>94441</td><td>70</td><td>41.68</td><td></td></tr></table><p>
fvp-unsat.2.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>2pipe.cnf</td><td>3944</td><td>1228</td><td>5</td><td>0.030</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>2342</td><td>1172</td><td>6</td><td>0.030</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>2714</td><td>1298</td><td>6</td><td>0.040</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>27451</td><td>7467</td><td>18</td><td>0.480</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>13031</td><td>6352</td><td>16</td><td>0.390</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>18726</td><td>8608</td><td>19</td><td>0.630</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>22206</td><td>9744</td><td>22</td><td>0.760</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>106099</td><td>21231</td><td>19</td><td>2.800</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>58457</td><td>26545</td><td>26</td><td>3.420</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>54502</td><td>22606</td><td>21</td><td>3.310</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>70512</td><td>27555</td><td>22</td><td>4.350</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>77375</td><td>27882</td><td>20</td><td>5.040</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>230894</td><td>16169</td><td>8</td><td>4.290</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>109835</td><td>44046</td><td>18</td><td>10.470</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>107762</td><td>38373</td><td>15</td><td>10.040</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>117212</td><td>41795</td><td>17</td><td>11.930</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>225310</td><td>85934</td><td>28</td><td>24.360</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>115593</td><td>35449</td><td>13</td><td>12.240</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td><td>765554</td><td>128571</td><td>24</td><td>50.930</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>344042</td><td>109757</td><td>16</td><td>57.360</td><td>UNSAT</td></tr>
<tr><td>7pipe.cnf</td><td>1311063</td><td>283785</td><td>28</td><td>169.210</td><td>UNSAT</td></tr>
<tr><td>7pipe_bug.cnf</td><td>794211</td><td>91521</td><td>9</td><td>65.460</td><td>SAT</td></tr>
<tr><td>Total (22 / 22)</td><td>4578835</td><td>1037088</td><td>376</td><td>437.57</td><td></td></tr></table><p>
fvp-unsat.3.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</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>11099896</td><td>1595388</td><td>103</td><td>2790.700</td><td>UNSAT</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 (1 / 6)</td><td>11099896</td><td>1595388</td><td>103</td><td>2790.7</td><td></td></tr></table><p>
liveness_sat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</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></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>2dlx_cc_ex_bp_f_bug10_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug1_liveness.cnf</td><td>515110</td><td>97797</td><td>5</td><td>415.860</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>365329</td><td>62623</td><td>4</td><td>288.030</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>1793818</td><td>435427</td><td>11</td><td>2402.340</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>1136072</td><td>254967</td><td>7</td><td>1363.760</td><td>SAT</td></tr>
<tr><td>Total (4 / 10)</td><td>3810329</td><td>850814</td><td>27</td><td>4469.99</td><td></td></tr></table><p>
liveness_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bp_f_liveness.cnf</td><td>154328</td><td>77374</td><td>48</td><td>21.150</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td><td>1557163</td><td>909913</td><td>174</td><td>772.660</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>171086</td><td>82115</td><td>30</td><td>35.010</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>41813</td><td>18487</td><td>22</td><td>2.320</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>1924390</td><td>1087889</td><td>274</td><td>831.14</td><td></td></tr></table><p>
liveness_unsat_2.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bp_u_f_liveness.cnf</td><td>46693</td><td>16480</td><td>20</td><td>2.280</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>196627</td><td>87044</td><td>38</td><td>27.270</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>131742</td><td>62702</td><td>23</td><td>19.390</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>375062</td><td>166226</td><td>81</td><td>48.94</td><td></td></tr></table><p>
npe-1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bug_no_pe.cnf</td><td>544</td><td>47</td><td>1</td><td>0.010</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>230181</td><td>162434</td><td>296</td><td>24.920</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf</td><td>381300</td><td>107125</td><td>7</td><td>187.450</td><td>SAT</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></tr>
<tr><td>9dlx_vliw_at_bp_mc2_no_pe.cnf</td></td></tr>
<tr><td>Total (3 / 6)</td><td>612025</td><td>269606</td><td>304</td><td>212.38</td><td></td></tr></table><p>
pipe_ooo_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</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></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>2786</td><td>1384</td><td>7</td><td>0.040</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>27480</td><td>12719</td><td>26</td><td>1.030</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>96284</td><td>37332</td><td>30</td><td>7.040</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>287825</td><td>101522</td><td>36</td><td>37.220</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>805160</td><td>301387</td><td>52</td><td>172.970</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo.cnf</td><td>2176848</td><td>851290</td><td>80</td><td>814.060</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo.cnf</td><td>4960036</td><td>1856263</td><td>103</td><td>2598.620</td><td>UNSAT</td></tr>
<tr><td>9pipe_9_ooo.cnf</td><td>4115975</td><td>1446053</td><td>52</td><td>2599.650</td><td>UNSAT</td></tr>
<tr><td>Total (8 / 15)</td><td>12472394</td><td>4607950</td><td>386</td><td>6230.63</td><td></td></tr></table><p>
pipe_ooo_unsat_1.1
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</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>4354</td><td>1737</td><td>8</td><td>0.050</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>32108</td><td>9029</td><td>21</td><td>0.610</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>103046</td><td>22642</td><td>24</td><td>3.390</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td><td>301603</td><td>47724</td><td>22</td><td>14.530</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td><td>755819</td><td>103658</td><td>25</td><td>54.420</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td><td>1855147</td><td>238276</td><td>32</td><td>196.720</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td><td>4419711</td><td>647958</td><td>50</td><td>745.860</td><td>UNSAT</td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td><td>4896882</td><td>513530</td><td>27</td><td>815.650</td><td>UNSAT</td></tr>
<tr><td>Total (8 / 14)</td><td>12368670</td><td>1584554</td><td>209</td><td>1831.23</td><td></td></tr></table><p>
pipe_sat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug1.cnf</td></td></tr>
<tr><td>12pipe_bug10.cnf</td><td>388014</td><td>46530</td><td>1</td><td>249.930</td><td>SAT</td></tr>
<tr><td>12pipe_bug2.cnf</td><td>338142</td><td>40425</td><td>1</td><td>214.840</td><td>SAT</td></tr>
<tr><td>12pipe_bug3.cnf</td></td></tr>
<tr><td>12pipe_bug4.cnf</td><td>914571</td><td>153325</td><td>4</td><td>673.170</td><td>SAT</td></tr>
<tr><td>12pipe_bug5.cnf</td></td></tr>
<tr><td>12pipe_bug6.cnf</td><td>452</td><td>40</td><td>1</td><td>3.790</td><td>SAT</td></tr>
<tr><td>12pipe_bug7.cnf</td></td></tr>
<tr><td>12pipe_bug8.cnf</td><td>17256</td><td>1054</td><td>1</td><td>12.960</td><td>SAT</td></tr>
<tr><td>12pipe_bug9.cnf</td></td></tr>
<tr><td>Total (5 / 10)</td><td>1658435</td><td>241374</td><td>8</td><td>1154.69</td><td></td></tr></table><p>
pipe_sat_1.1
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug10_q0.cnf</td><td>63619</td><td>4532</td><td>1</td><td>29.170</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td><td>304685</td><td>23283</td><td>1</td><td>147.460</td><td>SAT</td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>342257</td><td>26867</td><td>1</td><td>167.030</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>268586</td><td>24946</td><td>1</td><td>144.450</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>237913</td><td>14701</td><td>2</td><td>96.480</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>2892236</td><td>329481</td><td>8</td><td>1730.160</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>108162</td><td>7226</td><td>1</td><td>48.320</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>2549606</td><td>283885</td><td>7</td><td>1505.800</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td><td>10920</td><td>676</td><td>1</td><td>5.820</td><td>SAT</td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>2843561</td><td>323160</td><td>7</td><td>1690.430</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td>9621545</td><td>1038757</td><td>30</td><td>5565.12</td><td></td></tr></table><p>
pipe_unsat_1.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_k.cnf</td><td>3468</td><td>1399</td><td>8</td><td>0.040</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>22987</td><td>7961</td><td>17</td><td>0.530</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td><td>93106</td><td>25692</td><td>23</td><td>3.270</td><td>UNSAT</td></tr>
<tr><td>05pipe_k.cnf</td><td>243498</td><td>44525</td><td>18</td><td>10.980</td><td>UNSAT</td></tr>
<tr><td>06pipe_k.cnf</td><td>381865</td><td>28187</td><td>7</td><td>12.460</td><td>UNSAT</td></tr>
<tr><td>07pipe_k.cnf</td><td>1675238</td><td>386730</td><td>36</td><td>271.510</td><td>UNSAT</td></tr>
<tr><td>08pipe_k.cnf</td><td>2881023</td><td>555634</td><td>30</td><td>506.610</td><td>UNSAT</td></tr>
<tr><td>09pipe_k.cnf</td><td>3158415</td><td>118383</td><td>6</td><td>202.320</td><td>UNSAT</td></tr>
<tr><td>10pipe_k.cnf</td><td>9554261</td><td>1432480</td><td>32</td><td>2682.420</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>18013861</td><td>2600991</td><td>177</td><td>3690.14</td><td></td></tr></table><p>
pipe_unsat_1.1
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_q0_k.cnf</td><td>3792</td><td>1293</td><td>5</td><td>0.040</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>24049</td><td>6312</td><td>14</td><td>0.390</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>84172</td><td>15549</td><td>16</td><td>2.060</td><td>UNSAT</td></tr>
<tr><td>05pipe_q0_k.cnf</td><td>255168</td><td>32799</td><td>15</td><td>8.900</td><td>UNSAT</td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>427805</td><td>25183</td><td>7</td><td>15.790</td><td>UNSAT</td></tr>
<tr><td>07pipe_q0_k.cnf</td><td>1061437</td><td>86101</td><td>11</td><td>66.120</td><td>UNSAT</td></tr>
<tr><td>08pipe_q0_k.cnf</td><td>1811419</td><td>112051</td><td>10</td><td>138.460</td><td>UNSAT</td></tr>
<tr><td>09pipe_q0_k.cnf</td><td>3002400</td><td>79843</td><td>5</td><td>289.970</td><td>UNSAT</td></tr>
<tr><td>10pipe_q0_k.cnf</td><td>5243509</td><td>235504</td><td>9</td><td>656.820</td><td>UNSAT</td></tr>
<tr><td>11pipe_q0_k.cnf</td><td>8651593</td><td>290846</td><td>8</td><td>1271.050</td><td>UNSAT</td></tr>
<tr><td>12pipe_q0_k.cnf</td><td>14292081</td><td>419761</td><td>10</td><td>2545.670</td><td>UNSAT</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 (11 / 14)</td><td>34857425</td><td>1305242</td><td>110</td><td>4995.27</td><td></td></tr></table><p>
vliw_sat_2.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</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>86242</td><td>923</td><td>1</td><td>68.600</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug3.cnf</td><td>6174591</td><td>516201</td><td>13</td><td>2379.740</td><td>SAT</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>733694</td><td>35132</td><td>3</td><td>357.420</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>5451217</td><td>444824</td><td>12</td><td>1663.110</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>7136117</td><td>597539</td><td>15</td><td>2680.690</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td></td></tr>
<tr><td>Total (5 / 9)</td><td>19581861</td><td>1594619</td><td>44</td><td>7149.56</td><td></td></tr></table><p>
vliw_sat_2.1
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</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>726016</td><td>29937</td><td>3</td><td>622.010</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug8.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug9.cnf</td></td></tr>
<tr><td>Total (1 / 10)</td><td>726016</td><td>29937</td><td>3</td><td>622.01</td><td></td></tr></table><p>
vliw_sat_4.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug1.cnf</td><td>5383465</td><td>143444</td><td>5</td><td>2957.080</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>1606489</td><td>15853</td><td>2</td><td>1085.900</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>1722056</td><td>14077</td><td>3</td><td>1206.640</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>2723276</td><td>31674</td><td>3</td><td>1720.640</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>3893464</td><td>73367</td><td>3</td><td>2198.530</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>5048678</td><td>159602</td><td>6</td><td>2869.850</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>966048</td><td>6208</td><td>2</td><td>719.330</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>2189689</td><td>21693</td><td>2</td><td>1453.120</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>3848466</td><td>83817</td><td>3</td><td>2324.830</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>3194660</td><td>54471</td><td>4</td><td>1981.430</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td>30576291</td><td>604206</td><td>33</td><td>18517.35</td><td></td></tr></table><p>
vliw_unsat_2.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq1.cnf</td><td>3633371</td><td>199044</td><td>51</td><td>112.540</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td><td>10253447</td><td>357412</td><td>46</td><td>428.760</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td><td>20402798</td><td>512304</td><td>38</td><td>1104.630</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq4.cnf</td><td>44138768</td><td>835052</td><td>38</td><td>3252.160</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>78428384</td><td>1903812</td><td>173</td><td>4898.09</td><td></td></tr></table><p>
vliw_unsat_3.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24_D.cnf</td></td></tr>
<tr><td>Total (0 / 2)</td><td></td><td></td><td></td><td>0</td><td></td></tr></table><p>
vliw_unsat_4.0
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>9vliw_m_9stages_C1.cnf</td><td>4784887</td><td>479450</td><td>20</td><td>829.600</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>4784887</td><td>479450</td><td>20</td><td>829.6</td><td></td></tr></table><p>