Tinisat, using restart policy (Luby's, unit=8)<p>
22 groups, 251 instances, 2-hour cutoff<p>
Instances solved: 179 (67 SAT + 112 UNSAT)<br>
Time: 690874 seconds / 191.91 hours / 8.00 days<br>
Time on solved instances: 172474 seconds (52359 SAT + 120115 UNSAT)<p>
Instances solved in 10 minutes: 117 (13232 seconds)<br>
Instances solved in 15 minutes: 125 (19434 seconds)<br>
Instances solved in 20 minutes: 133 (27454 seconds)<br>
Instances solved in 30 minutes: 145 (44986 seconds)<br>
Instances solved in 60 minutes: 165 (100429 seconds)<br>
Instances solved in 90 minutes: 175 (145669 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>32</td><td>/</td><td>32</td><td width=20></td><td>75105.95</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>3096.78</td></tr>
<tr><td>fvp-sat.3.0</td><td width=20></td><td>15</td><td>/</td><td>20</td><td width=20></td><td>8503.94</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>50.97</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>475.87</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>6176.61</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>1351.05</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>71.91</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>546.43</td></tr>
<tr><td>pipe_ooo_unsat_1.0</td><td width=20></td><td>7</td><td>/</td><td>15</td><td width=20></td><td>7353.73</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>2779.31</td></tr>
<tr><td>pipe_sat_1.0</td><td width=20></td><td>10</td><td>/</td><td>10</td><td width=20></td><td>6705.27</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>2085.46</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>10</td><td>/</td><td>13</td><td width=20></td><td>5449.42</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>12</td><td>/</td><td>14</td><td width=20></td><td>13484.05</td></tr>
<tr><td>vliw_sat_2.0</td><td width=20></td><td>8</td><td>/</td><td>9</td><td width=20></td><td>15435.9</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>3444.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>2292.16</td></tr>
<tr><td>vliw_unsat_2.0</td><td width=20></td><td>3</td><td>/</td><td>9</td><td width=20></td><td>10253.39</td></tr>
<tr><td>vliw_unsat_3.0</td><td width=20></td><td>1</td><td>/</td><td>2</td><td width=20></td><td>6514.75</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>1297.02</td></tr>
</table>
<p>

dlx_iq_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>260240</td><td>3617585</td><td>5794959</td><td>162431</td><td>4023</td><td>1020.53</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>276124</td><td>3861235</td><td>6713624</td><td>177998</td><td>4093</td><td>1181.79</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td><td>292635</td><td>4115946</td><td>7465760</td><td>188248</td><td>4094</td><td>1286.33</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td><td>309785</td><td>4381995</td><td>7867361</td><td>199003</td><td>4203</td><td>1439.72</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td><td>327586</td><td>4659661</td><td>8389237</td><td>202074</td><td>4306</td><td>1526.18</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td><td>346050</td><td>4949225</td><td>9369723</td><td>208129</td><td>4476</td><td>1661.41</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td><td>365189</td><td>5250970</td><td>9734829</td><td>213414</td><td>4605</td><td>1794.14</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td><td>385015</td><td>5565181</td><td>10411819</td><td>215875</td><td>4651</td><td>1925.17</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td><td>405540</td><td>5892145</td><td>10849298</td><td>225876</td><td>4984</td><td>2105.36</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td><td>426776</td><td>6232151</td><td>12063328</td><td>240406</td><td>5243</td><td>2376.00</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>143519</td><td>1877765</td><td>2678836</td><td>105503</td><td>2556</td><td>387.70</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td><td>448735</td><td>6585490</td><td>12743646</td><td>246604</td><td>5418</td><td>2504.70</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq53_a.cnf</td><td>471429</td><td>6952455</td><td>14429993</td><td>255511</td><td>5628</td><td>2805.56</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq54_a.cnf</td><td>663574</td><td>15489863</td><td>13688361</td><td>285559</td><td>6141</td><td>4330.24</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq55_a.cnf</td><td>519070</td><td>7728445</td><td>16234592</td><td>270657</td><td>6136</td><td>3248.03</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq56_a.cnf</td><td>544041</td><td>8138066</td><td>16861363</td><td>298733</td><td>6538</td><td>3525.22</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq57_a.cnf</td><td>569795</td><td>8562505</td><td>18076198</td><td>288126</td><td>6204</td><td>3666.49</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq58_a.cnf</td><td>596344</td><td>9002065</td><td>20080701</td><td>318151</td><td>7096</td><td>4228.86</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq59_a.cnf</td><td>623700</td><td>9457051</td><td>21491151</td><td>329488</td><td>7244</td><td>4541.75</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq60_a.cnf</td><td>651875</td><td>9927770</td><td>22229984</td><td>330088</td><td>7273</td><td>4760.47</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq61_a.cnf</td><td>673311</td><td>10435991</td><td>10546922</td><td>195262</td><td>4094</td><td>2836.00</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq34_a.cnf</td><td>154300</td><td>2034001</td><td>2922244</td><td>113465</td><td>2747</td><td>448.81</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq62_a.cnf</td><td>710730</td><td>10917645</td><td>25082333</td><td>327685</td><td>7165</td><td>5288.51</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq63_a.cnf</td><td>720715</td><td>11606548</td><td>17195218</td><td>281496</td><td>6141</td><td>4383.90</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq64_a.cnf</td><td>773005</td><td>11974186</td><td>27783611</td><td>392771</td><td>8189</td><td>6389.10</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq35_a.cnf</td><td>165600</td><td>2198895</td><td>3260643</td><td>118037</td><td>2875</td><td>480.76</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td><td>228994</td><td>4194027</td><td>3716746</td><td>130996</td><td>3069</td><td>794.66</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td><td>245646</td><td>4568332</td><td>4020414</td><td>131451</td><td>3094</td><td>848.12</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>202734</td><td>2748125</td><td>4320050</td><td>142580</td><td>3451</td><td>722.23</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>216230</td><td>2950261</td><td>4501972</td><td>139704</td><td>3353</td><td>740.67</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>230305</td><td>3162370</td><td>4946374</td><td>150531</td><td>3637</td><td>853.72</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td><td>244971</td><td>3384721</td><td>5938961</td><td>162417</td><td>4023</td><td>1003.82</td><td>UNSAT</td></tr>
<tr><td>Total (32 / 32)</td><td colspan=2></td><td>361410251</td><td>7048269</td><td>156750</td><td>75105.95</td><td></td></tr></table><p>
engine_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>engine_4.cnf</td><td>6944</td><td>66654</td><td>60493</td><td>32858</td><td>1016</td><td>15.61</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>7000</td><td>67586</td><td>187376</td><td>114725</td><td>2807</td><td>98.41</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td><td>18788</td><td>214095</td><td>990601</td><td>629510</td><td>12539</td><td>2271.88</td><td>UNSAT</td></tr>
<tr><td>engine_5_case1.cnf</td><td>18810</td><td>214185</td><td>21622</td><td>12061</td><td>399</td><td>8.79</td><td>UNSAT</td></tr>
<tr><td>engine_5_nd.cnf</td><td>18878</td><td>216156</td></td></tr>
<tr><td>engine_5_nd_case1.cnf</td><td>18900</td><td>216246</td><td>67156</td><td>41295</td><td>1044</td><td>36.70</td><td>UNSAT</td></tr>
<tr><td>engine_6.cnf</td><td>45276</td><td>605958</td></td></tr>
<tr><td>engine_6_case1.cnf</td><td>45303</td><td>606068</td><td>78645</td><td>47959</td><td>1276</td><td>79.40</td><td>UNSAT</td></tr>
<tr><td>engine_6_nd.cnf</td><td>45408</td><td>610010</td></td></tr>
<tr><td>engine_6_nd_case1.cnf</td><td>45435</td><td>610120</td><td>337936</td><td>227021</td><td>5002</td><td>585.99</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 10)</td><td colspan=2></td><td>1743829</td><td>1105429</td><td>24083</td><td>3096.78</td><td></td></tr></table><p>
fvp-sat.3.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>35853</td><td>1012270</td><td>3523653</td><td>125802</td><td>3068</td><td>144.42</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td><td>35853</td><td>1012271</td><td>2207026</td><td>87298</td><td>2046</td><td>88.21</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>35947</td><td>992674</td><td>202615</td><td>539</td><td>30</td><td>3.35</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>35854</td><td>1012315</td><td>508119</td><td>4824</td><td>188</td><td>9.35</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug05.cnf</td><td>35853</td><td>1012271</td></td></tr>
<tr><td>pipe_64_4_bug06.cnf</td><td>35853</td><td>1012271</td><td>4013643</td><td>195471</td><td>4094</td><td>222.83</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug07.cnf</td><td>35853</td><td>1012271</td><td>13468908</td><td>867888</td><td>16382</td><td>2303.51</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>35622</td><td>1003074</td><td>9416</td><td>12</td><td>1</td><td>1.96</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>35726</td><td>1011764</td><td>2915969</td><td>85982</td><td>2046</td><td>85.62</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>35839</td><td>1012135</td><td>13604</td><td>13</td><td>1</td><td>2.00</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>35853</td><td>1012271</td></td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>35854</td><td>1012275</td><td>4784472</td><td>326912</td><td>7164</td><td>492.69</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>35855</td><td>1012302</td><td>14953332</td><td>1384063</td><td>25596</td><td>4886.44</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>35855</td><td>1012407</td><td>13341</td><td>14</td><td>1</td><td>1.99</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td><td>35853</td><td>1012271</td><td>2451963</td><td>88156</td><td>2046</td><td>90.96</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>35853</td><td>1012271</td><td>2385354</td><td>80847</td><td>2045</td><td>86.47</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug17.cnf</td><td>35853</td><td>1012271</td></td></tr>
<tr><td>pipe_64_4_bug18.cnf</td><td>35853</td><td>1012271</td></td></tr>
<tr><td>pipe_64_4_bug19.cnf</td><td>35852</td><td>1012266</td></td></tr>
<tr><td>pipe_64_4_bug20.cnf</td><td>35853</td><td>1012271</td><td>2259415</td><td>84862</td><td>2046</td><td>84.14</td><td>SAT</td></tr>
<tr><td>Total (15 / 20)</td><td colspan=2></td><td>53710830</td><td>3332683</td><td>66754</td><td>8503.94</td><td></td></tr></table><p>
fvp-unsat.1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>776</td><td>3725</td><td>2497</td><td>684</td><td>35</td><td>0.02</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_mc_ex_bp_f.cnf</td><td>3250</td><td>24640</td><td>21192</td><td>4595</td><td>182</td><td>0.44</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>4583</td><td>41704</td><td>34701</td><td>8287</td><td>261</td><td>1.19</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>20093</td><td>179492</td><td>529379</td><td>88618</td><td>2046</td><td>49.32</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td colspan=2></td><td>587769</td><td>102184</td><td>2524</td><td>50.97</td><td></td></tr></table><p>
fvp-unsat.2.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>2pipe.cnf</td><td>892</td><td>6695</td><td>3027</td><td>1078</td><td>59</td><td>0.05</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>834</td><td>7026</td><td>3017</td><td>1184</td><td>61</td><td>0.05</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>925</td><td>8213</td><td>3502</td><td>1387</td><td>62</td><td>0.07</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>2468</td><td>27533</td><td>23748</td><td>6315</td><td>251</td><td>0.65</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>2223</td><td>26561</td><td>15017</td><td>5033</td><td>189</td><td>0.49</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>2400</td><td>29981</td><td>25576</td><td>9335</td><td>315</td><td>1.14</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2577</td><td>33270</td><td>27839</td><td>9847</td><td>327</td><td>1.25</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>5237</td><td>80213</td><td>79234</td><td>17525</td><td>510</td><td>4.21</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>4647</td><td>74554</td><td>60126</td><td>18458</td><td>513</td><td>4.48</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>4941</td><td>82207</td><td>75348</td><td>24996</td><td>763</td><td>6.86</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>5233</td><td>89473</td><td>86014</td><td>24103</td><td>731</td><td>6.92</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>5525</td><td>96480</td><td>102061</td><td>27003</td><td>790</td><td>8.64</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>9471</td><td>195452</td><td>120531</td><td>10770</td><td>376</td><td>4.09</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>8441</td><td>187545</td><td>119364</td><td>31236</td><td>949</td><td>14.11</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>8851</td><td>201796</td><td>132466</td><td>32051</td><td>976</td><td>15.24</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>9267</td><td>215440</td><td>136348</td><td>29315</td><td>890</td><td>15.21</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>9764</td><td>221405</td><td>282061</td><td>64355</td><td>1723</td><td>41.52</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>10113</td><td>240892</td><td>144112</td><td>28158</td><td>828</td><td>16.19</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td><td>15800</td><td>394739</td><td>479897</td><td>69471</td><td>1873</td><td>60.81</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>17064</td><td>545612</td><td>392359</td><td>75711</td><td>2043</td><td>78.42</td><td>UNSAT</td></tr>
<tr><td>7pipe.cnf</td><td>23910</td><td>751118</td><td>976253</td><td>129806</td><td>3069</td><td>185.00</td><td>UNSAT</td></tr>
<tr><td>7pipe_bug.cnf</td><td>24065</td><td>731850</td><td>159168</td><td>11806</td><td>384</td><td>10.47</td><td>SAT</td></tr>
<tr><td>Total (22 / 22)</td><td colspan=2></td><td>3447068</td><td>628943</td><td>17682</td><td>475.87</td><td></td></tr></table><p>
fvp-unsat.3.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>40347</td><td>1224040</td></td></tr>
<tr><td>pipe_64_02.cnf</td><td>41774</td><td>1269338</td></td></tr>
<tr><td>pipe_64_04.cnf</td><td>35853</td><td>1012270</td></td></tr>
<tr><td>pipe_64_08.cnf</td><td>50879</td><td>1622874</td></td></tr>
<tr><td>pipe_64_16.cnf</td><td>64262</td><td>2291120</td></td></tr>
<tr><td>pipe_64_32.cnf</td><td>95179</td><td>4396018</td></td></tr>
<tr><td>Total (0 / 6)</td><td colspan=2></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>Vars</td><td>Clauses</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>292249</td><td>4906188</td><td>830631</td><td>119908</td><td>2939</td><td>951.56</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td><td>331848</td><td>5706594</td><td>336858</td><td>37113</td><td>1022</td><td>343.31</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug7_liveness.cnf</td><td>375775</td><td>6617342</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug8_liveness.cnf</td><td>424320</td><td>7649214</td><td>1960705</td><td>324632</td><td>7164</td><td>3473.71</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug9_liveness.cnf</td><td>477782</td><td>8813656</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug10_liveness.cnf</td><td>536469</td><td>10122798</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug1_liveness.cnf</td><td>171648</td><td>2614464</td><td>141009</td><td>15697</td><td>509</td><td>93.86</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>196655</td><td>3068742</td><td>428137</td><td>55840</td><td>1531</td><td>343.70</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>224920</td><td>3596474</td><td>604623</td><td>84131</td><td>2046</td><td>547.60</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>256697</td><td>4205986</td><td>454921</td><td>55936</td><td>1531</td><td>422.87</td><td>SAT</td></tr>
<tr><td>Total (7 / 10)</td><td colspan=2></td><td>4756884</td><td>693257</td><td>16742</td><td>6176.61</td><td></td></tr></table><p>
liveness_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>9474</td><td>107213</td><td>150485</td><td>64067</td><td>1721</td><td>42.87</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td><td>24104</td><td>339857</td><td>858641</td><td>410880</td><td>8190</td><td>1264.45</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>18274</td><td>202528</td><td>128982</td><td>49926</td><td>1319</td><td>40.01</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>6128</td><td>65112</td><td>38492</td><td>14683</td><td>507</td><td>3.72</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_bp_f_liveness.cnf</td><td>202253</td><td>4313014</td></td></tr>
<tr><td>2dlx_ca_ex_bp_f_liveness.cnf</td><td>421107</td><td>8754014</td></td></tr>
<tr><td>2dlx_ca_ex_liveness.cnf</td><td>318771</td><td>7410689</td></td></tr>
<tr><td>2dlx_ca_liveness.cnf</td><td>115049</td><td>2148917</td></td></tr>
<tr><td>2dlx_cc_bp_f_liveness.cnf</td><td>267364</td><td>6003507</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_liveness.cnf</td><td>600698</td><td>11589474</td></td></tr>
<tr><td>2dlx_cc_ex_liveness.cnf</td><td>352057</td><td>7935053</td></td></tr>
<tr><td>2dlx_cc_liveness.cnf</td><td>122395</td><td>2149255</td></td></tr>
<tr><td>Total (4 / 12)</td><td colspan=2></td><td>1176600</td><td>539556</td><td>11737</td><td>1351.05</td><td></td></tr></table><p>
liveness_unsat_2.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>6874</td><td>65479</td><td>52024</td><td>16407</td><td>510</td><td>4.30</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>14628</td><td>161477</td><td>159541</td><td>58663</td><td>1533</td><td>37.97</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>16011</td><td>210685</td><td>114354</td><td>42821</td><td>1107</td><td>29.64</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_bp_u_f_liveness.cnf</td><td>121388</td><td>2001843</td></td></tr>
<tr><td>2dlx_ca_ex_bp_u_f_liveness.cnf</td><td>223527</td><td>3922017</td></td></tr>
<tr><td>2dlx_ca_ex_d_liveness.cnf</td><td>235853</td><td>5459971</td></td></tr>
<tr><td>2dlx_cc_bp_u_f_liveness.cnf</td><td>144071</td><td>2411213</td></td></tr>
<tr><td>2dlx_cc_ex_bp_u_f_liveness.cnf</td><td>258649</td><td>4520142</td></td></tr>
<tr><td>2dlx_cc_ex_d_liveness.cnf</td><td>266476</td><td>6144987</td></td></tr>
<tr><td>Total (3 / 9)</td><td colspan=2></td><td>325919</td><td>117891</td><td>3150</td><td>71.91</td><td></td></tr></table><p>
npe-1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>3295</td><td>35409</td><td>4211</td><td>814</td><td>44</td><td>0.14</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>3295</td><td>35410</td><td>160573</td><td>94814</td><td>2234</td><td>61.27</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf</td><td>96675</td><td>1401773</td><td>693846</td><td>154269</td><td>3769</td><td>485.02</td><td>SAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_no_pe.cnf</td><td>96675</td><td>1401773</td></td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf</td><td>889302</td><td>14582074</td></td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_no_pe.cnf</td><td>889302</td><td>14582081</td></td></tr>
<tr><td>Total (3 / 6)</td><td colspan=2></td><td>858630</td><td>249897</td><td>6047</td><td>546.43</td><td></td></tr></table><p>
pipe_ooo_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>67050</td><td>2862719</td></td></tr>
<tr><td>11pipe_11_ooo.cnf</td><td>88289</td><td>4187694</td></td></tr>
<tr><td>12pipe_12_ooo.cnf</td><td>113768</td><td>5954744</td></td></tr>
<tr><td>13pipe_13_ooo.cnf</td><td>143311</td><td>8409838</td></td></tr>
<tr><td>14pipe_14_ooo.cnf</td><td>179056</td><td>11185426</td></td></tr>
<tr><td>15pipe_15_ooo.cnf</td><td>219755</td><td>14874914</td></td></tr>
<tr><td>16pipe_16_ooo.cnf</td><td>266498</td><td>19470237</td></td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>918</td><td>8109</td><td>4283</td><td>1635</td><td>70</td><td>0.08</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2533</td><td>32182</td><td>32974</td><td>11999</td><td>396</td><td>1.56</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>5356</td><td>89506</td><td>141219</td><td>49608</td><td>1307</td><td>17.59</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>9705</td><td>200959</td><td>385886</td><td>115076</td><td>2810</td><td>77.12</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>15948</td><td>397032</td><td>1032408</td><td>305425</td><td>6670</td><td>435.83</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo.cnf</td><td>24415</td><td>711050</td><td>2975381</td><td>931365</td><td>16858</td><td>2943.09</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo.cnf</td><td>35510</td><td>1191215</td></td></tr>
<tr><td>9pipe_9_ooo.cnf</td><td>49309</td><td>1924020</td><td>4256802</td><td>984367</td><td>18171</td><td>3878.46</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 15)</td><td colspan=2></td><td>8828953</td><td>2399475</td><td>46282</td><td>7353.73</td><td></td></tr></table><p>
pipe_ooo_unsat_1.1
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>81932</td><td>2080755</td></td></tr>
<tr><td>11pipe_11_ooo_q0_T0.cnf</td><td>110150</td><td>3003049</td></td></tr>
<tr><td>12pipe_12_ooo_q0_T0.cnf</td><td>144721</td><td>4206416</td></td></tr>
<tr><td>13pipe_13_ooo_q0_T0.cnf</td><td>185924</td><td>5911016</td></td></tr>
<tr><td>14pipe_14_ooo_q0_T0.cnf</td><td>236250</td><td>7676928</td></td></tr>
<tr><td>15pipe_15_ooo_q0_T0.cnf</td><td>294982</td><td>10067733</td></td></tr>
<tr><td>2pipe_2_ooo_q0_T0.cnf</td><td>895</td><td>6561</td><td>3648</td><td>1238</td><td>61</td><td>0.05</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>2566</td><td>25625</td><td>29464</td><td>8880</td><td>290</td><td>0.86</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>5605</td><td>70042</td><td>103075</td><td>24574</td><td>756</td><td>5.46</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td><td>10482</td><td>156027</td><td>324544</td><td>67087</td><td>1788</td><td>32.06</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td><td>17710</td><td>304026</td><td>689317</td><td>107360</td><td>2557</td><td>81.45</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td><td>27846</td><td>538853</td><td>1565901</td><td>248731</td><td>5498</td><td>325.09</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td><td>41491</td><td>889823</td><td>3368879</td><td>495708</td><td>10073</td><td>1059.96</td><td>UNSAT</td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td><td>59024</td><td>1430330</td><td>3512339</td><td>507861</td><td>10236</td><td>1274.38</td><td>UNSAT</td></tr>
<tr><td>Total (8 / 14)</td><td colspan=2></td><td>9597167</td><td>1461439</td><td>31259</td><td>2779.31</td><td></td></tr></table><p>
pipe_sat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>12pipe_bug1.cnf</td><td>118040</td><td>8804672</td><td>1361123</td><td>157765</td><td>3842</td><td>945.30</td><td>SAT</td></tr>
<tr><td>12pipe_bug10.cnf</td><td>118040</td><td>8804672</td><td>2592502</td><td>341039</td><td>7614</td><td>2160.87</td><td>SAT</td></tr>
<tr><td>12pipe_bug2.cnf</td><td>118040</td><td>8804630</td><td>480932</td><td>53178</td><td>1433</td><td>330.56</td><td>SAT</td></tr>
<tr><td>12pipe_bug3.cnf</td><td>118039</td><td>8804669</td><td>1975696</td><td>250949</td><td>5569</td><td>1522.64</td><td>SAT</td></tr>
<tr><td>12pipe_bug4.cnf</td><td>117504</td><td>8743027</td><td>88156</td><td>3622</td><td>130</td><td>42.79</td><td>SAT</td></tr>
<tr><td>12pipe_bug5.cnf</td><td>118040</td><td>8804672</td><td>401326</td><td>40984</td><td>1025</td><td>247.93</td><td>SAT</td></tr>
<tr><td>12pipe_bug6.cnf</td><td>117665</td><td>8647068</td><td>5477</td><td>0</td><td>0</td><td>16.42</td><td>SAT</td></tr>
<tr><td>12pipe_bug7.cnf</td><td>118040</td><td>8804672</td><td>1771728</td><td>232807</td><td>5116</td><td>1378.45</td><td>SAT</td></tr>
<tr><td>12pipe_bug8.cnf</td><td>117526</td><td>8760516</td><td>24093</td><td>16</td><td>2</td><td>17.27</td><td>SAT</td></tr>
<tr><td>12pipe_bug9.cnf</td><td>118038</td><td>8780591</td><td>88642</td><td>3615</td><td>129</td><td>43.04</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>8789675</td><td>1083975</td><td>24860</td><td>6705.27</td><td></td></tr></table><p>
pipe_sat_1.1
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>138918</td><td>4678760</td><td>679648</td><td>50713</td><td>1343</td><td>256.91</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td><td>138917</td><td>4678756</td><td>174010</td><td>10593</td><td>363</td><td>61.99</td><td>SAT</td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>138918</td><td>4678718</td><td>276163</td><td>15088</td><td>508</td><td>88.02</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>138917</td><td>4678757</td><td>1521145</td><td>133677</td><td>3192</td><td>682.05</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>138563</td><td>4675040</td><td>52972</td><td>1154</td><td>61</td><td>14.52</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>138918</td><td>4678760</td><td>431907</td><td>31055</td><td>938</td><td>174.14</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>138795</td><td>4671352</td><td>68296</td><td>1742</td><td>77</td><td>18.22</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>138918</td><td>4678760</td><td>1225350</td><td>105455</td><td>2555</td><td>552.18</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td><td>138711</td><td>4688614</td><td>26322</td><td>491</td><td>29</td><td>10.68</td><td>SAT</td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>138916</td><td>4676007</td><td>565402</td><td>43995</td><td>1148</td><td>226.75</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>5021215</td><td>393963</td><td>10214</td><td>2085.46</td><td></td></tr></table><p>
pipe_unsat_1.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>02pipe_k.cnf</td><td>860</td><td>6693</td><td>3287</td><td>1222</td><td>61</td><td>0.05</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>2391</td><td>27405</td><td>23196</td><td>6221</td><td>250</td><td>0.62</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td><td>5095</td><td>79489</td><td>84384</td><td>20126</td><td>586</td><td>5.26</td><td>UNSAT</td></tr>
<tr><td>05pipe_k.cnf</td><td>9330</td><td>189109</td><td>215869</td><td>38311</td><td>1022</td><td>18.12</td><td>UNSAT</td></tr>
<tr><td>06pipe_k.cnf</td><td>15346</td><td>408792</td><td>295539</td><td>18885</td><td>540</td><td>12.21</td><td>UNSAT</td></tr>
<tr><td>07pipe_k.cnf</td><td>23909</td><td>751116</td><td>1004713</td><td>132385</td><td>3132</td><td>189.53</td><td>UNSAT</td></tr>
<tr><td>08pipe_k.cnf</td><td>35065</td><td>1332773</td><td>1637141</td><td>174987</td><td>4093</td><td>348.85</td><td>UNSAT</td></tr>
<tr><td>09pipe_k.cnf</td><td>49112</td><td>2317839</td><td>1849149</td><td>69581</td><td>1881</td><td>149.82</td><td>UNSAT</td></tr>
<tr><td>10pipe_k.cnf</td><td>67300</td><td>3601247</td><td>4523763</td><td>381824</td><td>8189</td><td>1454.02</td><td>UNSAT</td></tr>
<tr><td>11pipe_k.cnf</td><td>89315</td><td>5584003</td><td>7509252</td><td>556861</td><td>11260</td><td>3270.94</td><td>UNSAT</td></tr>
<tr><td>12pipe_k.cnf</td><td>115915</td><td>8395649</td></td></tr>
<tr><td>13pipe_k.cnf</td><td>147626</td><td>12295313</td></td></tr>
<tr><td>14pipe_k.cnf</td><td>184980</td><td>17597059</td></td></tr>
<tr><td>Total (10 / 13)</td><td colspan=2></td><td>17146293</td><td>1400403</td><td>31014</td><td>5449.42</td><td></td></tr></table><p>
pipe_unsat_1.1
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>873</td><td>6457</td><td>3450</td><td>1351</td><td>62</td><td>0.05</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>2476</td><td>25181</td><td>19593</td><td>5798</td><td>224</td><td>0.50</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>5380</td><td>69072</td><td>73109</td><td>17973</td><td>510</td><td>3.42</td><td>UNSAT</td></tr>
<tr><td>05pipe_q0_k.cnf</td><td>10026</td><td>154409</td><td>205780</td><td>35624</td><td>1021</td><td>12.93</td><td>UNSAT</td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>16775</td><td>315960</td><td>278760</td><td>18239</td><td>510</td><td>11.08</td><td>UNSAT</td></tr>
<tr><td>07pipe_q0_k.cnf</td><td>26512</td><td>536414</td><td>882628</td><td>109234</td><td>2594</td><td>96.13</td><td>UNSAT</td></tr>
<tr><td>08pipe_q0_k.cnf</td><td>39434</td><td>887706</td><td>1548066</td><td>196709</td><td>4102</td><td>253.91</td><td>UNSAT</td></tr>
<tr><td>09pipe_q0_k.cnf</td><td>55996</td><td>1468197</td><td>1634287</td><td>65058</td><td>1754</td><td>113.59</td><td>UNSAT</td></tr>
<tr><td>10pipe_q0_k.cnf</td><td>77639</td><td>2082017</td><td>4285612</td><td>404906</td><td>8190</td><td>952.24</td><td>UNSAT</td></tr>
<tr><td>11pipe_q0_k.cnf</td><td>104244</td><td>3007883</td><td>6747245</td><td>549704</td><td>11257</td><td>1633.73</td><td>UNSAT</td></tr>
<tr><td>12pipe_q0_k.cnf</td><td>136800</td><td>4216460</td><td>11098416</td><td>795048</td><td>16379</td><td>3226.72</td><td>UNSAT</td></tr>
<tr><td>13pipe_q0_k.cnf</td><td>176066</td><td>5761591</td><td>16833918</td><td>1335437</td><td>24573</td><td>7179.75</td><td>UNSAT</td></tr>
<tr><td>14pipe_q0_k.cnf</td><td>222845</td><td>7702617</td></td></tr>
<tr><td>15pipe_q0_k.cnf</td><td>277976</td><td>10103924</td></td></tr>
<tr><td>Total (12 / 14)</td><td colspan=2></td><td>43610864</td><td>3535081</td><td>71176</td><td>13484.05</td><td></td></tr></table><p>
vliw_sat_2.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>236038</td><td>8084666</td><td>8957860</td><td>462521</td><td>9212</td><td>2388.22</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug2.cnf</td><td>235928</td><td>8076545</td><td>74614</td><td>32</td><td>3</td><td>18.28</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug3.cnf</td><td>235402</td><td>8060882</td><td>10592398</td><td>853026</td><td>16382</td><td>5275.35</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug4.cnf</td><td>235277</td><td>8063780</td><td>8428514</td><td>513064</td><td>10237</td><td>2691.97</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug5.cnf</td><td>235923</td><td>8076534</td><td>8337230</td><td>610985</td><td>12285</td><td>3425.71</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>235926</td><td>8076539</td><td>1229163</td><td>2072</td><td>93</td><td>55.77</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>173811</td><td>5609632</td><td>4284491</td><td>169050</td><td>4092</td><td>676.20</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>229942</td><td>7882655</td><td>4499305</td><td>204743</td><td>4349</td><td>904.40</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td><td>235184</td><td>8063818</td></td></tr>
<tr><td>Total (8 / 9)</td><td colspan=2></td><td>46403575</td><td>2815493</td><td>56653</td><td>15435.9</td><td></td></tr></table><p>
vliw_sat_2.1
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>410707</td><td>15613033</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug10.cnf</td><td>408558</td><td>15554750</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug2.cnf</td><td>409731</td><td>15576332</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug3.cnf</td><td>410219</td><td>15596614</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug4.cnf</td><td>409220</td><td>15574959</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug5.cnf</td><td>410693</td><td>15615653</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug6.cnf</td><td>410553</td><td>15598521</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug7.cnf</td><td>410729</td><td>15606974</td><td>1955957</td><td>4306</td><td>164</td><td>131.75</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug8.cnf</td><td>410560</td><td>15603495</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug9.cnf</td><td>449867</td><td>16331249</td><td>19079996</td><td>385858</td><td>8189</td><td>3312.26</td><td>SAT</td></tr>
<tr><td>Total (2 / 10)</td><td colspan=2></td><td>21035953</td><td>390164</td><td>8353</td><td>3444.01</td><td></td></tr></table><p>
vliw_sat_4.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>521188</td><td>13378641</td><td>5608015</td><td>14303</td><td>497</td><td>234.16</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>521182</td><td>13378625</td><td>4678343</td><td>11639</td><td>381</td><td>198.84</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>521158</td><td>13378532</td><td>4927469</td><td>8351</td><td>267</td><td>164.43</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>521046</td><td>13376161</td><td>4818092</td><td>6385</td><td>251</td><td>158.10</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>520721</td><td>13348117</td><td>5186943</td><td>16757</td><td>510</td><td>255.11</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>520770</td><td>13380350</td><td>6177916</td><td>37411</td><td>1022</td><td>430.82</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>521192</td><td>13378781</td><td>5221473</td><td>9394</td><td>316</td><td>180.74</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>521147</td><td>13378010</td><td>4776586</td><td>9164</td><td>307</td><td>176.62</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>521179</td><td>13378617</td><td>5027403</td><td>15811</td><td>509</td><td>249.10</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>521187</td><td>13378624</td><td>5256051</td><td>15051</td><td>508</td><td>244.24</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>51678291</td><td>144266</td><td>4568</td><td>2292.16</td><td></td></tr></table><p>
vliw_unsat_2.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>24604</td><td>261473</td><td>2446213</td><td>544583</td><td>11088</td><td>884.45</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td><td>44095</td><td>542253</td><td>5491905</td><td>967434</td><td>17703</td><td>2647.77</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td><td>69789</td><td>968295</td><td>10907041</td><td>1589775</td><td>29977</td><td>6721.17</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq4.cnf</td><td>106013</td><td>1598301</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq5.cnf</td><td>151669</td><td>2465731</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6.cnf</td><td>209724</td><td>3634677</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq7.cnf</td><td>306095</td><td>6069108</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8.cnf</td><td>371419</td><td>7170909</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq9.cnf</td><td>482093</td><td>9676386</td></td></tr>
<tr><td>Total (3 / 9)</td><td colspan=2></td><td>18845159</td><td>3101792</td><td>58768</td><td>10253.39</td><td></td></tr></table><p>
vliw_unsat_3.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>132413</td><td>1435600</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24_D.cnf</td><td>132156</td><td>1434887</td><td>43498061</td><td>1455197</td><td>27258</td><td>6514.75</td><td>UNSAT</td></tr>
<tr><td>Total (1 / 2)</td><td colspan=2></td><td>43498061</td><td>1455197</td><td>27258</td><td>6514.75</td><td></td></tr></table><p>
vliw_unsat_4.0
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>96177</td><td>1814189</td><td>5557217</td><td>524161</td><td>10492</td><td>1297.02</td><td>UNSAT</td></tr>
<tr><td>9vliw_m_9stages_iq1_C1.cnf</td><td>154309</td><td>3230738</td></td></tr>
<tr><td>9vliw_m_9stages_iq2_C1.cnf</td><td>230662</td><td>5267084</td></td></tr>
<tr><td>9vliw_m_9stages_iq3_C1.cnf</td><td>333336</td><td>8122058</td></td></tr>
<tr><td>Total (1 / 4)</td><td colspan=2></td><td>5557217</td><td>524161</td><td>10492</td><td>1297.02</td><td></td></tr></table><p>