MiniSat v1.14<p>
22 groups, 251 instances, 2-hour cutoff<p>
Instances solved: 128 (55 SAT + 73 UNSAT)<br>
Time: 989001 seconds / 274.72 hours / 11.45 days<br>
Time on solved instances: 103401 seconds (18210 SAT + 85192 UNSAT)<p>
Instances solved in 10 minutes: 95 (5216 seconds)<br>
Instances solved in 15 minutes: 98 (7659 seconds)<br>
Instances solved in 20 minutes: 98 (7659 seconds)<br>
Instances solved in 30 minutes: 106 (19950 seconds)<br>
Instances solved in 60 minutes: 116 (46376 seconds)<br>
Instances solved in 90 minutes: 125 (85946 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>23</td><td>/</td><td>32</td><td width=20></td><td>75784.33</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>2040.1584</td></tr>
<tr><td>fvp-sat.3.0</td><td width=20></td><td>11</td><td>/</td><td>20</td><td width=20></td><td>5316.16768</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>64.458193</td></tr>
<tr><td>fvp-unsat.2.0</td><td width=20></td><td>20</td><td>/</td><td>22</td><td width=20></td><td>3223.807045</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>7</td><td>/</td><td>10</td><td width=20></td><td>6156.3959</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>5493.7489</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>139.72576</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>25.161162</td></tr>
<tr><td>pipe_ooo_unsat_1.0</td><td width=20></td><td>3</td><td>/</td><td>15</td><td width=20></td><td>419.897418</td></tr>
<tr><td>pipe_ooo_unsat_1.1</td><td width=20></td><td>3</td><td>/</td><td>14</td><td width=20></td><td>242.066793</td></tr>
<tr><td>pipe_sat_1.0</td><td width=20></td><td>6</td><td>/</td><td>10</td><td width=20></td><td>94.7787</td></tr>
<tr><td>pipe_sat_1.1</td><td width=20></td><td>8</td><td>/</td><td>10</td><td width=20></td><td>241.91059</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>4</td><td>/</td><td>13</td><td width=20></td><td>187.385304</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>4</td><td>/</td><td>14</td><td width=20></td><td>1144.345663</td></tr>
<tr><td>vliw_sat_2.0</td><td width=20></td><td>6</td><td>/</td><td>9</td><td width=20></td><td>1526.355</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>920.6993</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>379.9613</td></tr>
<tr><td>vliw_unsat_2.0</td><td width=20></td><td>0</td><td>/</td><td>9</td><td width=20></td><td>0</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>0</td><td>/</td><td>4</td><td width=20></td><td>0</td></tr>
</table>
<p>

dlx_iq_unsat_1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_iq42_a.cnf</td><td>20</td><td>550672</td><td>5149688</td><td>1648.83</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>21</td><td>930699</td><td>8776771</td><td>3392.45</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td><td>21</td><td>816481</td><td>8493561</td><td>3299.54</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td><td>21</td><td>836165</td><td>8858423</td><td>3276.2</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td><td>21</td><td>688825</td><td>7543598</td><td>3034.86</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td><td>22</td><td>1003741</td><td>10737552</td><td>4294.25</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td><td>21</td><td>878480</td><td>9227952</td><td>4187.96</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td><td>22</td><td>1233208</td><td>14497776</td><td>5454.98</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td><td>22</td><td>1050642</td><td>11260763</td><td>5738.08</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>20</td><td>622493</td><td>5340078</td><td>1495.69</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td><td>22</td><td>1120811</td><td>14529149</td><td>6262.52</td><td>UNSAT</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>21</td><td>962380</td><td>12804309</td><td>4928.68</td><td>UNSAT</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>21</td><td>794425</td><td>10401157</td><td>5228.96</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq60_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq61_a.cnf</td><td>19</td><td>326224</td><td>3516968</td><td>1866.64</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq34_a.cnf</td><td>21</td><td>853518</td><td>6351597</td><td>2196.65</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq62_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq63_a.cnf</td><td>19</td><td>308702</td><td>3637229</td><td>1698.6</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq64_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq35_a.cnf</td><td>21</td><td>704596</td><td>5360912</td><td>1568.92</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td><td>22</td><td>1441150</td><td>8596393</td><td>4494.52</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td><td>23</td><td>1581637</td><td>7857779</td><td>3825.34</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>20</td><td>546816</td><td>5846747</td><td>1432.01</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>20</td><td>618333</td><td>5573137</td><td>1488.17</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>20</td><td>618149</td><td>6450380</td><td>2023.8</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td><td>21</td><td>788855</td><td>8229361</td><td>2946.68</td><td>UNSAT</td></tr>
<tr><td>Total (23 / 32)</td><td>481</td><td>19277002</td><td>189041280</td><td>75784.33</td><td></td></tr></table><p>
engine_unsat_1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>engine_4.cnf</td><td>13</td><td>37526</td><td>70027</td><td>11.3663</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>16</td><td>125968</td><td>204684</td><td>63.1084</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td><td>21</td><td>832940</td><td>1274788</td><td>1649.32</td><td>UNSAT</td></tr>
<tr><td>engine_5_case1.cnf</td><td>12</td><td>17149</td><td>38395</td><td>6.554</td><td>UNSAT</td></tr>
<tr><td>engine_5_nd.cnf</td></td></tr>
<tr><td>engine_5_nd_case1.cnf</td><td>14</td><td>43822</td><td>90170</td><td>20.8738</td><td>UNSAT</td></tr>
<tr><td>engine_6.cnf</td></td></tr>
<tr><td>engine_6_case1.cnf</td><td>15</td><td>81846</td><td>171711</td><td>73.3189</td><td>UNSAT</td></tr>
<tr><td>engine_6_nd.cnf</td></td></tr>
<tr><td>engine_6_nd_case1.cnf</td><td>17</td><td>167310</td><td>345954</td><td>215.617</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 10)</td><td>108</td><td>1306561</td><td>2195729</td><td>2040.1584</td><td></td></tr></table><p>
fvp-sat.3.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>pipe_64_4_bug01.cnf</td><td>7</td><td>3212</td><td>185395</td><td>1.71774</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td></td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>3</td><td>429</td><td>164699</td><td>1.13083</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>14</td><td>39567</td><td>291872</td><td>8.01578</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug05.cnf</td></td></tr>
<tr><td>pipe_64_4_bug06.cnf</td></td></tr>
<tr><td>pipe_64_4_bug07.cnf</td></td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>20</td><td>452942</td><td>1604291</td><td>247.477</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>16</td><td>128314</td><td>594628</td><td>29.1636</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>21</td><td>894338</td><td>2650983</td><td>760.919</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>19</td><td>380110</td><td>1238656</td><td>162.029</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>13</td><td>36987</td><td>269484</td><td>7.05193</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>24</td><td>2268512</td><td>6468842</td><td>3756.49</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>18</td><td>211399</td><td>962912</td><td>67.3248</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td></td></tr>
<tr><td>pipe_64_4_bug16.cnf</td></td></tr>
<tr><td>pipe_64_4_bug17.cnf</td></td></tr>
<tr><td>pipe_64_4_bug18.cnf</td></td></tr>
<tr><td>pipe_64_4_bug19.cnf</td><td>20</td><td>469968</td><td>1515042</td><td>274.848</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug20.cnf</td></td></tr>
<tr><td>Total (11 / 20)</td><td>175</td><td>4885778</td><td>15946804</td><td>5316.16768</td><td></td></tr></table><p>
fvp-unsat.1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_mc_ex_bp_f.cnf</td><td>5</td><td>982</td><td>3670</td><td>0.024996</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_mc_ex_bp_f.cnf</td><td>9</td><td>6225</td><td>28502</td><td>0.408937</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>11</td><td>15175</td><td>52191</td><td>1.56676</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>17</td><td>182994</td><td>819290</td><td>62.4575</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td>42</td><td>205376</td><td>903653</td><td>64.458193</td><td></td></tr></table><p>
fvp-unsat.2.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>2pipe.cnf</td><td>7</td><td>2192</td><td>6672</td><td>0.06399</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>6</td><td>1666</td><td>4858</td><td>0.042993</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>6</td><td>1874</td><td>6340</td><td>0.057991</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>16</td><td>119104</td><td>287257</td><td>22.7035</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>11</td><td>15003</td><td>41460</td><td>0.939857</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>12</td><td>20986</td><td>58122</td><td>1.81872</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>12</td><td>24274</td><td>70800</td><td>2.72059</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>18</td><td>250194</td><td>675009</td><td>88.5935</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>14</td><td>45388</td><td>138002</td><td>7.19991</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>14</td><td>58141</td><td>200287</td><td>11.2013</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>17</td><td>160254</td><td>431679</td><td>52.559</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>19</td><td>329854</td><td>875063</td><td>157.214</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>18</td><td>280118</td><td>655436</td><td>165.498</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>16</td><td>87473</td><td>320769</td><td>29.1156</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>17</td><td>159623</td><td>469851</td><td>74.1507</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>15</td><td>60142</td><td>294011</td><td>16.2435</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>23</td><td>1756928</td><td>4435647</td><td>2015.81</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>19</td><td>299487</td><td>806858</td><td>199.608</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td></td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>18</td><td>285326</td><td>1482527</td><td>377.573</td><td>UNSAT</td></tr>
<tr><td>7pipe.cnf</td></td></tr>
<tr><td>7pipe_bug.cnf</td><td>5</td><td>861</td><td>29240</td><td>0.692894</td><td>SAT</td></tr>
<tr><td>Total (20 / 22)</td><td>283</td><td>3958888</td><td>11289888</td><td>3223.807045</td><td></td></tr></table><p>
fvp-unsat.3.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</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></td><td></td><td>0</td><td></td></tr></table><p>
liveness_sat_1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</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>10</td><td>7797</td><td>181480</td><td>15.3397</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>9</td><td>6464</td><td>194989</td><td>15.4077</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>8</td><td>4285</td><td>140026</td><td>11.5083</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>12</td><td>17543</td><td>407154</td><td>45.2631</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug5_liveness.cnf</td><td>10</td><td>9431</td><td>279219</td><td>25.8271</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td><td>21</td><td>700024</td><td>4518814</td><td>3670.21</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug7_liveness.cnf</td><td>20</td><td>493298</td><td>3499950</td><td>2372.84</td><td>SAT</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 (7 / 10)</td><td>90</td><td>1238842</td><td>9221632</td><td>6156.3959</td><td></td></tr></table><p>
liveness_unsat_1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bp_f_liveness.cnf</td><td>19</td><td>309683</td><td>743820</td><td>249.863</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td><td>23</td><td>1649691</td><td>3604877</td><td>5183.79</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>15</td><td>83053</td><td>261877</td><td>48.0287</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>14</td><td>49616</td><td>137877</td><td>12.0672</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>71</td><td>2092043</td><td>4748451</td><td>5493.7489</td><td></td></tr></table><p>
liveness_unsat_2.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bp_u_f_liveness.cnf</td><td>13</td><td>37293</td><td>118665</td><td>7.49086</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>16</td><td>128657</td><td>361651</td><td>73.0819</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>16</td><td>102409</td><td>291604</td><td>59.153</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>45</td><td>268359</td><td>771920</td><td>139.72576</td><td></td></tr></table><p>
npe-1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>1dlx_c_bug_no_pe.cnf</td><td>3</td><td>421</td><td>6868</td><td>0.049992</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>15</td><td>75593</td><td>162752</td><td>17.7023</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf</td><td>9</td><td>5557</td><td>280753</td><td>7.40887</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>27</td><td>81571</td><td>450373</td><td>25.161162</td><td></td></tr></table><p>
pipe_ooo_unsat_1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</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>8</td><td>3891</td><td>10053</td><td>0.141978</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>13</td><td>32963</td><td>93801</td><td>3.67744</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>21</td><td>816084</td><td>2072731</td><td>416.078</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td></td></tr>
<tr><td>6pipe_6_ooo.cnf</td></td></tr>
<tr><td>7pipe_7_ooo.cnf</td></td></tr>
<tr><td>8pipe_8_ooo.cnf</td></td></tr>
<tr><td>9pipe_9_ooo.cnf</td></td></tr>
<tr><td>Total (3 / 15)</td><td>42</td><td>852938</td><td>2176585</td><td>419.897418</td><td></td></tr></table><p>
pipe_ooo_unsat_1.1
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</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>6</td><td>1443</td><td>5287</td><td>0.039993</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>12</td><td>18567</td><td>52142</td><td>1.3028</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>20</td><td>615035</td><td>1450245</td><td>240.724</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td></td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td></td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td></td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td></td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td></td></tr>
<tr><td>Total (3 / 14)</td><td>38</td><td>635045</td><td>1507674</td><td>242.066793</td><td></td></tr></table><p>
pipe_sat_1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug1.cnf</td><td>9</td><td>6342</td><td>99188</td><td>16.6395</td><td>SAT</td></tr>
<tr><td>12pipe_bug10.cnf</td><td>14</td><td>41230</td><td>325611</td><td>36.4645</td><td>SAT</td></tr>
<tr><td>12pipe_bug2.cnf</td><td>3</td><td>358</td><td>60123</td><td>6.78297</td><td>SAT</td></tr>
<tr><td>12pipe_bug3.cnf</td></td></tr>
<tr><td>12pipe_bug4.cnf</td></td></tr>
<tr><td>12pipe_bug5.cnf</td><td>7</td><td>3123</td><td>91193</td><td>12.4161</td><td>SAT</td></tr>
<tr><td>12pipe_bug6.cnf</td></td></tr>
<tr><td>12pipe_bug7.cnf</td><td>10</td><td>7725</td><td>124294</td><td>14.7498</td><td>SAT</td></tr>
<tr><td>12pipe_bug8.cnf</td></td></tr>
<tr><td>12pipe_bug9.cnf</td><td>5</td><td>966</td><td>62018</td><td>7.72583</td><td>SAT</td></tr>
<tr><td>Total (6 / 10)</td><td>48</td><td>59744</td><td>762427</td><td>94.7787</td><td></td></tr></table><p>
pipe_sat_1.1
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug10_q0.cnf</td><td>4</td><td>728</td><td>100855</td><td>5.66814</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td></td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>5</td><td>1109</td><td>91088</td><td>5.44717</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>9</td><td>5116</td><td>144182</td><td>7.8878</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>18</td><td>198045</td><td>1063753</td><td>199.76</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>4</td><td>609</td><td>96065</td><td>5.41418</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>8</td><td>4013</td><td>133394</td><td>7.93379</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>4</td><td>722</td><td>100618</td><td>5.61715</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td></td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>3</td><td>463</td><td>75689</td><td>4.18236</td><td>SAT</td></tr>
<tr><td>Total (8 / 10)</td><td>55</td><td>210805</td><td>1805644</td><td>241.91059</td><td></td></tr></table><p>
pipe_unsat_1.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_k.cnf</td><td>8</td><td>3382</td><td>9409</td><td>0.101984</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>12</td><td>20012</td><td>64084</td><td>1.85472</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td><td>16</td><td>104840</td><td>268795</td><td>28.7026</td><td>UNSAT</td></tr>
<tr><td>05pipe_k.cnf</td></td></tr>
<tr><td>06pipe_k.cnf</td><td>19</td><td>295993</td><td>873217</td><td>156.726</td><td>UNSAT</td></tr>
<tr><td>07pipe_k.cnf</td></td></tr>
<tr><td>08pipe_k.cnf</td></td></tr>
<tr><td>09pipe_k.cnf</td></td></tr>
<tr><td>10pipe_k.cnf</td></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 (4 / 13)</td><td>55</td><td>424227</td><td>1215505</td><td>187.385304</td><td></td></tr></table><p>
pipe_unsat_1.1
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_q0_k.cnf</td><td>6</td><td>1660</td><td>4924</td><td>0.042993</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>12</td><td>25403</td><td>64042</td><td>2.17167</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>23</td><td>1737679</td><td>3541396</td><td>857.924</td><td>UNSAT</td></tr>
<tr><td>05pipe_q0_k.cnf</td></td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>19</td><td>362423</td><td>1110374</td><td>284.207</td><td>UNSAT</td></tr>
<tr><td>07pipe_q0_k.cnf</td></td></tr>
<tr><td>08pipe_q0_k.cnf</td></td></tr>
<tr><td>09pipe_q0_k.cnf</td></td></tr>
<tr><td>10pipe_q0_k.cnf</td></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 (4 / 14)</td><td>60</td><td>2127165</td><td>4720736</td><td>1144.345663</td><td></td></tr></table><p>
vliw_sat_2.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</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>4</td><td>708</td><td>389644</td><td>16.5555</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>21</td><td>666530</td><td>4253898</td><td>1309.79</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>10</td><td>7638</td><td>461317</td><td>43.5124</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>12</td><td>25584</td><td>684765</td><td>66.9198</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>9</td><td>5207</td><td>396811</td><td>32.0121</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td><td>13</td><td>28584</td><td>698669</td><td>57.5652</td><td>SAT</td></tr>
<tr><td>Total (6 / 9)</td><td>69</td><td>734251</td><td>6885104</td><td>1526.355</td><td></td></tr></table><p>
vliw_sat_2.1
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</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>19</td><td>304563</td><td>2985522</td><td>823.713</td><td>SAT</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>11</td><td>13579</td><td>966976</td><td>96.9863</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 (2 / 10)</td><td>30</td><td>318142</td><td>3952498</td><td>920.6993</td><td></td></tr></table><p>
vliw_sat_4.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug1.cnf</td><td>11</td><td>11849</td><td>1572673</td><td>41.1937</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>8</td><td>3458</td><td>1445549</td><td>26.8679</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>9</td><td>5267</td><td>1226865</td><td>30.9663</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>8</td><td>3412</td><td>1769256</td><td>24.4513</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>9</td><td>7329</td><td>1396599</td><td>42.3296</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>13</td><td>36652</td><td>2664512</td><td>89.5094</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>7</td><td>2677</td><td>1030496</td><td>21.4557</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>9</td><td>7362</td><td>1103707</td><td>29.1526</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>9</td><td>4972</td><td>1473338</td><td>26.534</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>10</td><td>9734</td><td>2054319</td><td>47.5008</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td>93</td><td>92712</td><td>15737314</td><td>379.9613</td><td></td></tr></table><p>
vliw_unsat_2.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>9dlx_vliw_at_b_iq1.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq4.cnf</td></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 (0 / 9)</td><td></td><td></td><td></td><td>0</td><td></td></tr></table><p>
vliw_unsat_3.0
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</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>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>9vliw_m_9stages_C1.cnf</td></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 (0 / 4)</td><td></td><td></td><td></td><td>0</td><td></td></tr></table><p>