MiniSat 2.0<p>
22 groups, 251 instances, 1-hour cutoff<p>
Instances solved: 102 (56 SAT + 46 UNSAT)<br>
Time: 558505 seconds / 155.14 hours / 6.46 days<br>
Time on solved instances: 22105 seconds (12955 SAT + 9149 UNSAT)<p>
Instances solved in 10 minutes: 92 (5517 seconds)<br>
Instances solved in 15 minutes: 93 (6199 seconds)<br>
Instances solved in 20 minutes: 93 (6199 seconds)<br>
Instances solved in 30 minutes: 97 (12208 seconds)<br>
Instances solved in 60 minutes: 102 (22105 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>2</td><td>/</td><td>32</td><td width=20></td><td>3541.18</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>2549.4522</td></tr>
<tr><td>fvp-sat.3.0</td><td width=20></td><td>13</td><td>/</td><td>20</td><td width=20></td><td>4078.3422</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>27.47585</td></tr>
<tr><td>fvp-unsat.2.0</td><td width=20></td><td>18</td><td>/</td><td>22</td><td width=20></td><td>3940.113206</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>6</td><td>/</td><td>10</td><td width=20></td><td>2589.4947</td></tr>
<tr><td>liveness_unsat_1.0</td><td width=20></td><td>3</td><td>/</td><td>12</td><td width=20></td><td>390.8488</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>205.849</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>111.935938</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>302.776586</td></tr>
<tr><td>pipe_ooo_unsat_1.1</td><td width=20></td><td>2</td><td>/</td><td>14</td><td width=20></td><td>2.158667</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>241.99416</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>173.56573</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>3</td><td>/</td><td>13</td><td width=20></td><td>1277.764129</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>3</td><td>/</td><td>14</td><td width=20></td><td>436.841868</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>879.6727</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>856.47</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>498.9896</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></tr>
<tr><td>1dlx_c_iq43_a.cnf</td></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></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>18</td><td>257407</td><td>2137281</td><td>1867.48</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq34_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq62_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq63_a.cnf</td><td>19</td><td>323526</td><td>2899366</td><td>1673.7</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq64_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq35_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td></td></tr>
<tr><td>Total (2 / 32)</td><td>37</td><td>580933</td><td>5036647</td><td>3541.18</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>34776</td><td>62969</td><td>12.3441</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>17</td><td>141463</td><td>211365</td><td>72.383</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td><td>22</td><td>1098511</td><td>1637910</td><td>2028.76</td><td>UNSAT</td></tr>
<tr><td>engine_5_case1.cnf</td><td>12</td><td>17484</td><td>36456</td><td>10.6854</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>43827</td><td>83516</td><td>30.7453</td><td>UNSAT</td></tr>
<tr><td>engine_6.cnf</td></td></tr>
<tr><td>engine_6_case1.cnf</td><td>14</td><td>55427</td><td>118264</td><td>69.6314</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>191774</td><td>356635</td><td>324.903</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 10)</td><td>109</td><td>1583262</td><td>2507115</td><td>2549.4522</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>13</td><td>26340</td><td>252471</td><td>16.3035</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>372</td><td>64265</td><td>11.1753</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>8</td><td>3461</td><td>103201</td><td>11.7892</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug05.cnf</td></td></tr>
<tr><td>pipe_64_4_bug06.cnf</td><td>18</td><td>220190</td><td>894127</td><td>95.7144</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug07.cnf</td></td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>8</td><td>4673</td><td>150650</td><td>11.8152</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>19</td><td>297349</td><td>1156422</td><td>140.438</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>10</td><td>10310</td><td>123761</td><td>12.2841</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>13</td><td>30839</td><td>279097</td><td>17.5433</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>13</td><td>32336</td><td>297199</td><td>17.2654</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>22</td><td>1279249</td><td>3872854</td><td>1765.86</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>15</td><td>62617</td><td>404793</td><td>24.6902</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td></td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>23</td><td>1561631</td><td>4685034</td><td>1924.46</td><td>SAT</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>15</td><td>73152</td><td>468328</td><td>29.0036</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug20.cnf</td></td></tr>
<tr><td>Total (13 / 20)</td><td>180</td><td>3602519</td><td>12752202</td><td>4078.3422</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>911</td><td>3224</td><td>0.031995</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_mc_ex_bp_f.cnf</td><td>10</td><td>11192</td><td>34833</td><td>0.952855</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>10</td><td>10625</td><td>38766</td><td>1.3258</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>15</td><td>84663</td><td>470383</td><td>25.1652</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td>40</td><td>107391</td><td>547206</td><td>27.47585</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>2296</td><td>6086</td><td>0.066989</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>6</td><td>1822</td><td>5037</td><td>0.054991</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>7</td><td>2633</td><td>6905</td><td>0.087986</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>13</td><td>26399</td><td>63222</td><td>2.35564</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>12</td><td>22911</td><td>52004</td><td>1.92471</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>11</td><td>15431</td><td>41437</td><td>1.09283</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>13</td><td>38608</td><td>94149</td><td>5.54816</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>24</td><td>2492596</td><td>4983260</td><td>1297.35</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>17</td><td>132055</td><td>352832</td><td>37.1014</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>17</td><td>147342</td><td>406605</td><td>49.9934</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>18</td><td>241863</td><td>682679</td><td>86.4889</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>18</td><td>235194</td><td>528641</td><td>84.6841</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>24</td><td>2463505</td><td>4637304</td><td>2019.76</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>16</td><td>105782</td><td>335296</td><td>36.2785</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>17</td><td>138563</td><td>438567</td><td>64.7132</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>18</td><td>222967</td><td>616933</td><td>127.055</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td></td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>18</td><td>232793</td><td>669654</td><td>115.119</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td></td></tr>
<tr><td>6pipe_6_ooo.cnf</td></td></tr>
<tr><td>7pipe.cnf</td></td></tr>
<tr><td>7pipe_bug.cnf</td><td>6</td><td>1505</td><td>29371</td><td>10.4384</td><td>SAT</td></tr>
<tr><td>Total (18 / 22)</td><td>262</td><td>6524265</td><td>13949982</td><td>3940.113206</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_bug5_liveness.cnf</td><td>12</td><td>22861</td><td>354933</td><td>106.991</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td><td>19</td><td>309596</td><td>2242394</td><td>2056.1</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>2dlx_cc_ex_bp_f_bug10_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug1_liveness.cnf</td><td>7</td><td>2260</td><td>85701</td><td>53.4369</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>10</td><td>8819</td><td>163526</td><td>89.6314</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>9</td><td>5915</td><td>147789</td><td>89.3204</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>14</td><td>39716</td><td>608913</td><td>194.015</td><td>SAT</td></tr>
<tr><td>Total (6 / 10)</td><td>71</td><td>389167</td><td>3603256</td><td>2589.4947</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>356579</td><td>809603</td><td>317.415</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td></td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>15</td><td>85054</td><td>253970</td><td>46.006</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>15</td><td>82826</td><td>220215</td><td>27.4278</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 (3 / 12)</td><td>49</td><td>524459</td><td>1283788</td><td>390.8488</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>14</td><td>43322</td><td>122460</td><td>11.0283</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>17</td><td>151312</td><td>415235</td><td>100.885</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>16</td><td>123444</td><td>344765</td><td>93.9357</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>47</td><td>318078</td><td>882460</td><td>205.849</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>6</td><td>1357</td><td>6885</td><td>0.405938</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>16</td><td>102440</td><td>194873</td><td>26.6559</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf</td><td>13</td><td>26511</td><td>278031</td><td>84.8741</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>35</td><td>130308</td><td>479789</td><td>111.935938</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>7</td><td>2739</td><td>7301</td><td>0.091986</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>16</td><td>109876</td><td>230455</td><td>15.8176</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>21</td><td>728973</td><td>1913470</td><td>286.867</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>44</td><td>841588</td><td>2151226</td><td>302.776586</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>7</td><td>2543</td><td>6583</td><td>0.084987</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>13</td><td>28749</td><td>70815</td><td>2.07368</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td></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 (2 / 14)</td><td>20</td><td>31292</td><td>77398</td><td>2.158667</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></tr>
<tr><td>12pipe_bug10.cnf</td></td></tr>
<tr><td>12pipe_bug2.cnf</td><td>8</td><td>4691</td><td>121750</td><td>11.4723</td><td>SAT</td></tr>
<tr><td>12pipe_bug3.cnf</td><td>17</td><td>131644</td><td>773915</td><td>197.048</td><td>SAT</td></tr>
<tr><td>12pipe_bug4.cnf</td><td>6</td><td>1734</td><td>68047</td><td>8.39972</td><td>SAT</td></tr>
<tr><td>12pipe_bug5.cnf</td><td>8</td><td>4719</td><td>85229</td><td>12.1861</td><td>SAT</td></tr>
<tr><td>12pipe_bug6.cnf</td><td>2</td><td>198</td><td>57229</td><td>6.34304</td><td>SAT</td></tr>
<tr><td>12pipe_bug7.cnf</td></td></tr>
<tr><td>12pipe_bug8.cnf</td></td></tr>
<tr><td>12pipe_bug9.cnf</td><td>4</td><td>799</td><td>60844</td><td>6.545</td><td>SAT</td></tr>
<tr><td>Total (6 / 10)</td><td>45</td><td>143785</td><td>1167014</td><td>241.99416</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>9</td><td>6792</td><td>185646</td><td>13.401</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td></td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>12</td><td>17465</td><td>234071</td><td>27.2359</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>11</td><td>11372</td><td>195308</td><td>18.4332</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>2</td><td>229</td><td>65053</td><td>4.31934</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>7</td><td>2310</td><td>115368</td><td>7.61584</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>9</td><td>4945</td><td>163712</td><td>10.7384</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>15</td><td>62323</td><td>541902</td><td>83.6223</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td></td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>8</td><td>3287</td><td>148153</td><td>8.19975</td><td>SAT</td></tr>
<tr><td>Total (8 / 10)</td><td>73</td><td>108723</td><td>1649213</td><td>173.56573</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>7</td><td>2280</td><td>6041</td><td>0.070989</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>14</td><td>49331</td><td>114887</td><td>5.64314</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td></td></tr>
<tr><td>05pipe_k.cnf</td></td></tr>
<tr><td>06pipe_k.cnf</td><td>22</td><td>1077615</td><td>2312424</td><td>1272.05</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 (3 / 13)</td><td>43</td><td>1129226</td><td>2433352</td><td>1277.764129</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>8</td><td>3817</td><td>8301</td><td>0.106983</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>11</td><td>11400</td><td>35797</td><td>0.752885</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td></td></tr>
<tr><td>05pipe_q0_k.cnf</td></td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>20</td><td>507448</td><td>1147068</td><td>435.982</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 (3 / 14)</td><td>39</td><td>522665</td><td>1191166</td><td>436.841868</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>6</td><td>2000</td><td>528486</td><td>38.3382</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>18</td><td>205046</td><td>2022875</td><td>487.977</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug5.cnf</td><td>14</td><td>42354</td><td>888305</td><td>148.833</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>15</td><td>58201</td><td>811101</td><td>128.652</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>10</td><td>9161</td><td>401912</td><td>31.2163</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>9</td><td>7244</td><td>412889</td><td>44.6562</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td></td></tr>
<tr><td>Total (6 / 9)</td><td>72</td><td>324006</td><td>5065568</td><td>879.6727</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>15</td><td>70222</td><td>1428421</td><td>681.933</td><td>SAT</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>12</td><td>17134</td><td>1021916</td><td>174.537</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>27</td><td>87356</td><td>2450337</td><td>856.47</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>10</td><td>7850</td><td>1423846</td><td>51.5442</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>10</td><td>7549</td><td>1162832</td><td>49.6405</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>8</td><td>3327</td><td>1462373</td><td>38.7991</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>9</td><td>6611</td><td>1402638</td><td>53.3989</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>8</td><td>4283</td><td>1367219</td><td>38.6121</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>7</td><td>2812</td><td>1184168</td><td>30.2304</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>10</td><td>8097</td><td>2088234</td><td>49.1965</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>8</td><td>3352</td><td>915151</td><td>37.9932</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>4</td><td>674</td><td>1166759</td><td>21.4897</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>13</td><td>29609</td><td>2070822</td><td>128.085</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td>87</td><td>74164</td><td>14244042</td><td>498.9896</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>