TiniSatELite<p>
22 groups, 251 instances, 1-hour cutoff<p>
Instances solved: 182 (75 SAT + 107 UNSAT)<br>
Time: 345948 seconds / 96.10 hours / 4.00 days<br>
Time on solved instances: 97548 seconds (37937 SAT + 59611 UNSAT)<p>
Instances solved in 10 minutes: 131 (18484 seconds)<br>
Instances solved in 15 minutes: 146 (29686 seconds)<br>
Instances solved in 20 minutes: 152 (35808 seconds)<br>
Instances solved in 30 minutes: 163 (52044 seconds)<br>
Instances solved in 60 minutes: 182 (97548 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>40331.0319</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>1434.712581</td></tr>
<tr><td>fvp-sat.3.0</td><td width=20></td><td>17</td><td>/</td><td>20</td><td width=20></td><td>1376.35018</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>30.599693</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>707.136284</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>8</td><td>/</td><td>10</td><td width=20></td><td>8422.6632</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>812.445301</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>61.332448</td></tr>
<tr><td>npe-1.0</td><td width=20></td><td>4</td><td>/</td><td>6</td><td width=20></td><td>1634.844436</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>4552.180187</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>2512.103376</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>6665.641</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>2586.6326</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>9</td><td>/</td><td>13</td><td width=20></td><td>4988.000376</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>9</td><td>/</td><td>14</td><td width=20></td><td>2721.016581</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>2808.4891</td></tr>
<tr><td>vliw_sat_2.1</td><td width=20></td><td>6</td><td>/</td><td>10</td><td width=20></td><td>7789.0365</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>3167.907</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>4337.39715</td></tr>
<tr><td>vliw_unsat_3.0</td><td width=20></td><td>0</td><td>/</td><td>2</td><td width=20></td><td>0</td></tr>
<tr><td>vliw_unsat_4.0</td><td width=20></td><td>1</td><td>/</td><td>4</td><td width=20></td><td>608.557</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>193146</td><td>3472159</td><td>5608595</td><td>193904</td><td>125</td><td>603.4689</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>204846</td><td>3706902</td><td>5278778</td><td>168581</td><td>123</td><td>559.5027</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td><td>217028</td><td>3952359</td><td>5949764</td><td>202151</td><td>126</td><td>746.9614</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td><td>229662</td><td>4209003</td><td>6047911</td><td>198969</td><td>126</td><td>692.2821</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td><td>242756</td><td>4476715</td><td>7119581</td><td>219030</td><td>126</td><td>822.0118</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td><td>256419</td><td>4756238</td><td>7241238</td><td>222063</td><td>126</td><td>870.0835</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td><td>270447</td><td>5047130</td><td>8385940</td><td>237387</td><td>136</td><td>993.4931</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td><td>285029</td><td>5350245</td><td>8729686</td><td>262135</td><td>156</td><td>1054.5937</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td><td>300152</td><td>5665713</td><td>9885189</td><td>260275</td><td>156</td><td>1159.7214</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td><td>315782</td><td>5994080</td><td>11169024</td><td>313952</td><td>189</td><td>1487.13</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>106920</td><td>1797260</td><td>2370789</td><td>122054</td><td>87</td><td>239.6788</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td><td>331938</td><td>6335262</td><td>11499581</td><td>278999</td><td>168</td><td>1354.5046</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq53_a.cnf</td><td>348514</td><td>6689197</td><td>11791822</td><td>295484</td><td>184</td><td>1554.816</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq54_a.cnf</td><td>535493</td><td>15219257</td><td>10268213</td><td>348445</td><td>211</td><td>2426.653</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq55_a.cnf</td><td>383616</td><td>7438996</td><td>14107620</td><td>328505</td><td>191</td><td>1890.3012</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq56_a.cnf</td><td>401887</td><td>7834511</td><td>14693700</td><td>324781</td><td>189</td><td>1902.6826</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq57_a.cnf</td><td>420833</td><td>8244707</td><td>15543853</td><td>369580</td><td>222</td><td>2121.2141</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq58_a.cnf</td><td>440345</td><td>8669567</td><td>15622352</td><td>358587</td><td>219</td><td>2202.1736</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq59_a.cnf</td><td>460437</td><td>9109336</td><td>17765982</td><td>362520</td><td>220</td><td>2277.209</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq60_a.cnf</td><td>481057</td><td>9564224</td><td>18185923</td><td>357846</td><td>219</td><td>2427.9193</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq61_a.cnf</td><td>501333</td><td>10069422</td><td>10052613</td><td>216141</td><td>126</td><td>1367.5896</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq34_a.cnf</td><td>114921</td><td>1947572</td><td>2786883</td><td>136190</td><td>93</td><td>280.1307</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq62_a.cnf</td><td>524220</td><td>10521275</td><td>19819472</td><td>381268</td><td>235</td><td>2801.9719</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq63_a.cnf</td><td>546359</td><td>11234647</td><td>13237552</td><td>284035</td><td>172</td><td>2121.0975</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq64_a.cnf</td><td>569891</td><td>11543182</td><td>22225203</td><td>397759</td><td>250</td><td>3115.9526</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq35_a.cnf</td><td>123270</td><td>2106034</td><td>2974840</td><td>141742</td><td>97</td><td>309.3095</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td><td>183939</td><td>4095710</td><td>2773127</td><td>157259</td><td>111</td><td>442.2723</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td><td>197384</td><td>4463267</td><td>3072456</td><td>162718</td><td>117</td><td>485.763</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>150705</td><td>2634725</td><td>3536918</td><td>157924</td><td>112</td><td>401.6358</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>160662</td><td>2829286</td><td>4564387</td><td>178438</td><td>124</td><td>487.7776</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>171042</td><td>3033427</td><td>4860923</td><td>190703</td><td>125</td><td>545.5744</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td><td>181905</td><td>3247867</td><td>5031721</td><td>197551</td><td>126</td><td>585.5562</td><td>UNSAT</td></tr>
<tr><td>Total (32 / 32)</td><td colspan=2></td><td>302201636</td><td>8026976</td><td>4987</td><td>40331.0319</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>5049</td><td>62239</td><td>54191</td><td>33744</td><td>30</td><td>9.951935</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>5106</td><td>63162</td><td>148716</td><td>106480</td><td>72</td><td>57.654936</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td><td>14254</td><td>204155</td><td>685164</td><td>497774</td><td>254</td><td>984.32075</td><td>UNSAT</td></tr>
<tr><td>engine_5_case1.cnf</td><td>14182</td><td>203731</td><td>18856</td><td>10830</td><td>13</td><td>6.65875</td><td>UNSAT</td></tr>
<tr><td>engine_5_nd.cnf</td><td>14344</td><td>206257</td></td></tr>
<tr><td>engine_5_nd_case1.cnf</td><td>14271</td><td>205823</td><td>55035</td><td>35180</td><td>30</td><td>20.47175</td><td>UNSAT</td></tr>
<tr><td>engine_6.cnf</td><td>35538</td><td>585934</td></td></tr>
<tr><td>engine_6_case1.cnf</td><td>35423</td><td>585231</td><td>73000</td><td>47850</td><td>39</td><td>55.43523</td><td>UNSAT</td></tr>
<tr><td>engine_6_nd.cnf</td><td>35670</td><td>589968</td></td></tr>
<tr><td>engine_6_nd_case1.cnf</td><td>35555</td><td>589248</td><td>267748</td><td>186599</td><td>125</td><td>300.21923</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 10)</td><td colspan=2></td><td>1302710</td><td>918457</td><td>563</td><td>1434.712581</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>30712</td><td>998061</td><td>67130</td><td>1091</td><td>2</td><td>4.9276</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td><td>30712</td><td>998062</td><td>398662</td><td>43879</td><td>35</td><td>18.6626</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>30425</td><td>977714</td><td>6943</td><td>26</td><td>0</td><td>4.1086</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>30713</td><td>998118</td><td>129650</td><td>7307</td><td>9</td><td>7.2196</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug05.cnf</td><td>30712</td><td>998062</td></td></tr>
<tr><td>pipe_64_4_bug06.cnf</td><td>30712</td><td>998048</td><td>1060476</td><td>172184</td><td>124</td><td>74.6576</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug07.cnf</td><td>30712</td><td>998048</td><td>2526396</td><td>517755</td><td>254</td><td>354.6696</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>30448</td><td>988766</td><td>12517</td><td>7</td><td>0</td><td>4.1326</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>30649</td><td>997679</td><td>117573</td><td>7845</td><td>9</td><td>7.18859</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>30699</td><td>997932</td><td>80894</td><td>1916</td><td>2</td><td>5.44859</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>30712</td><td>998047</td><td>1989456</td><td>382036</td><td>235</td><td>225.1946</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>30713</td><td>998052</td><td>235005</td><td>23361</td><td>23</td><td>11.2686</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>30714</td><td>998091</td><td>282434</td><td>48169</td><td>40</td><td>16.1166</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>30714</td><td>998196</td><td>118683</td><td>4041</td><td>5</td><td>5.7596</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td><td>30712</td><td>998048</td><td>2800395</td><td>578858</td><td>300</td><td>409.9966</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>30712</td><td>998062</td></td></tr>
<tr><td>pipe_64_4_bug17.cnf</td><td>30712</td><td>998062</td></td></tr>
<tr><td>pipe_64_4_bug18.cnf</td><td>30712</td><td>998062</td><td>1009351</td><td>169578</td><td>123</td><td>73.8796</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug19.cnf</td><td>30711</td><td>998050</td><td>550055</td><td>65459</td><td>55</td><td>29.0476</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug20.cnf</td><td>30712</td><td>998062</td><td>1474609</td><td>256526</td><td>155</td><td>124.0716</td><td>SAT</td></tr>
<tr><td>Total (17 / 20)</td><td colspan=2></td><td>12860229</td><td>2280038</td><td>1371</td><td>1376.35018</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>449</td><td>2916</td><td>2172</td><td>644</td><td>1</td><td>0.031996</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_mc_ex_bp_f.cnf</td><td>2146</td><td>22172</td><td>19346</td><td>4446</td><td>6</td><td>0.437972</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>3265</td><td>38744</td><td>32803</td><td>7021</td><td>8</td><td>0.895955</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>12650</td><td>163328</td><td>586898</td><td>88488</td><td>62</td><td>29.23377</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td colspan=2></td><td>641219</td><td>100599</td><td>77</td><td>30.599693</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>681</td><td>6165</td><td>3834</td><td>1384</td><td>2</td><td>0.070995</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>656</td><td>6422</td><td>2835</td><td>1483</td><td>2</td><td>0.071995</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>765</td><td>7839</td><td>3034</td><td>1253</td><td>2</td><td>0.079995</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>1973</td><td>26391</td><td>24705</td><td>9724</td><td>12</td><td>0.772976</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>1775</td><td>25204</td><td>13907</td><td>6389</td><td>7</td><td>0.522979</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>1938</td><td>28553</td><td>22298</td><td>8778</td><td>11</td><td>0.784976</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2096</td><td>31724</td><td>27057</td><td>11140</td><td>13</td><td>1.046974</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>4286</td><td>77945</td><td>113684</td><td>38218</td><td>30</td><td>6.873921</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>3754</td><td>71857</td><td>55042</td><td>21214</td><td>21</td><td>3.560928</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>4025</td><td>79387</td><td>85090</td><td>32030</td><td>29</td><td>6.043921</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>4294</td><td>86538</td><td>103574</td><td>38439</td><td>30</td><td>8.585912</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>4558</td><td>93382</td><td>117270</td><td>34463</td><td>30</td><td>7.522902</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>8052</td><td>190539</td><td>103853</td><td>14406</td><td>14</td><td>4.25082</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>7041</td><td>182710</td><td>109855</td><td>34594</td><td>30</td><td>11.63271</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>7418</td><td>196830</td><td>130900</td><td>34655</td><td>30</td><td>11.50476</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>7797</td><td>210359</td><td>140596</td><td>33625</td><td>30</td><td>12.00775</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>8055</td><td>216720</td><td>303307</td><td>92443</td><td>62</td><td>38.40475</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>8566</td><td>235539</td><td>149625</td><td>30565</td><td>29</td><td>11.60174</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td><td>13283</td><td>387485</td><td>671287</td><td>172890</td><td>124</td><td>108.34673</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>14349</td><td>536094</td><td>457869</td><td>82697</td><td>62</td><td>63.50272</td><td>UNSAT</td></tr>
<tr><td>7pipe.cnf</td><td>20670</td><td>739826</td><td>1473829</td><td>361719</td><td>220</td><td>388.4454</td><td>UNSAT</td></tr>
<tr><td>7pipe_bug.cnf</td><td>20392</td><td>720622</td><td>285384</td><td>40971</td><td>31</td><td>21.50043</td><td>SAT</td></tr>
<tr><td>Total (22 / 22)</td><td colspan=2></td><td>4398835</td><td>1103080</td><td>821</td><td>707.136284</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>36053</td><td>1211949</td></td></tr>
<tr><td>pipe_64_02.cnf</td><td>37330</td><td>1256937</td></td></tr>
<tr><td>pipe_64_04.cnf</td><td>30712</td><td>998061</td></td></tr>
<tr><td>pipe_64_08.cnf</td><td>45462</td><td>1608331</td></td></tr>
<tr><td>pipe_64_16.cnf</td><td>57279</td><td>2272949</td></td></tr>
<tr><td>pipe_64_32.cnf</td><td>84092</td><td>4367747</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>272555</td><td>4866520</td><td>2923618</td><td>567773</td><td>289</td><td>3334.6204</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td><td>310630</td><td>5663925</td><td>1027424</td><td>93565</td><td>62</td><td>563.4274</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug7_liveness.cnf</td><td>352911</td><td>6571431</td><td>2254139</td><td>340511</td><td>204</td><td>2122.3753</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug8_liveness.cnf</td><td>399694</td><td>7599826</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug9_liveness.cnf</td><td>451295</td><td>8760605</td><td>2082132</td><td>247376</td><td>144</td><td>1815.5235</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug10_liveness.cnf</td><td>507982</td><td>10065803</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug1_liveness.cnf</td><td>156911</td><td>2584548</td><td>56255</td><td>3926</td><td>5</td><td>38.258</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>180828</td><td>3036666</td><td>248669</td><td>17040</td><td>16</td><td>93.7555</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>207923</td><td>3562116</td><td>324245</td><td>29425</td><td>29</td><td>143.5029</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>238410</td><td>4169075</td><td>692037</td><td>61769</td><td>52</td><td>311.2002</td><td>SAT</td></tr>
<tr><td>Total (8 / 10)</td><td colspan=2></td><td>9608519</td><td>1361385</td><td>801</td><td>8422.6632</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>8078</td><td>104323</td><td>160266</td><td>74196</td><td>61</td><td>38.415874</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td><td>20884</td><td>332111</td><td>694335</td><td>356841</td><td>219</td><td>738.65771</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>14955</td><td>195986</td><td>124706</td><td>52992</td><td>44</td><td>32.01579</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>4955</td><td>62532</td><td>37736</td><td>17020</td><td>16</td><td>3.355927</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_bp_f_liveness.cnf</td><td>188087</td><td>4281700</td></td></tr>
<tr><td>2dlx_ca_ex_bp_f_liveness.cnf</td><td>395689</td><td>8701542</td></td></tr>
<tr><td>2dlx_ca_ex_liveness.cnf</td><td>295008</td><td>7363701</td></td></tr>
<tr><td>2dlx_ca_liveness.cnf</td><td>103371</td><td>2120692</td></td></tr>
<tr><td>2dlx_cc_bp_f_liveness.cnf</td><td>250175</td><td>5965651</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_liveness.cnf</td><td>570067</td><td>11528257</td></td></tr>
<tr><td>2dlx_cc_ex_liveness.cnf</td><td>323720</td><td>7879283</td></td></tr>
<tr><td>2dlx_cc_liveness.cnf</td><td>108753</td><td>2115636</td></td></tr>
<tr><td>Total (4 / 12)</td><td colspan=2></td><td>1017043</td><td>501049</td><td>340</td><td>812.445301</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>5412</td><td>62324</td><td>58704</td><td>23491</td><td>23</td><td>4.981938</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>11514</td><td>154193</td><td>153460</td><td>56808</td><td>45</td><td>27.2728</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>13130</td><td>204179</td><td>128342</td><td>53492</td><td>45</td><td>29.07771</td><td>UNSAT</td></tr>
<tr><td>2dlx_ca_bp_u_f_liveness.cnf</td><td>107982</td><td>1973576</td></td></tr>
<tr><td>2dlx_ca_ex_bp_u_f_liveness.cnf</td><td>200100</td><td>3874611</td></td></tr>
<tr><td>2dlx_ca_ex_d_liveness.cnf</td><td>214049</td><td>5409021</td></td></tr>
<tr><td>2dlx_cc_bp_u_f_liveness.cnf</td><td>127801</td><td>2376152</td></td></tr>
<tr><td>2dlx_cc_ex_bp_u_f_liveness.cnf</td><td>230220</td><td>4463153</td></td></tr>
<tr><td>2dlx_cc_ex_d_liveness.cnf</td><td>240576</td><td>6085970</td></td></tr>
<tr><td>Total (3 / 9)</td><td colspan=2></td><td>340506</td><td>133791</td><td>113</td><td>61.332448</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>2974</td><td>34392</td><td>2730</td><td>749</td><td>1</td><td>0.317968</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>2974</td><td>34393</td><td>117845</td><td>70158</td><td>60</td><td>24.658968</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf</td><td>93887</td><td>1395303</td><td>199714</td><td>16269</td><td>14</td><td>52.6505</td><td>SAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_no_pe.cnf</td><td>93887</td><td>1395284</td></td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf</td><td>879854</td><td>14559286</td><td>1557320</td><td>41753</td><td>32</td><td>1557.217</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_no_pe.cnf</td><td>879854</td><td>14559226</td></td></tr>
<tr><td>Total (4 / 6)</td><td colspan=2></td><td>1877609</td><td>128929</td><td>107</td><td>1634.844436</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>58916</td><td>2837433</td></td></tr>
<tr><td>11pipe_11_ooo.cnf</td><td>77804</td><td>4155136</td></td></tr>
<tr><td>12pipe_12_ooo.cnf</td><td>101195</td><td>5923947</td></td></tr>
<tr><td>13pipe_13_ooo.cnf</td><td>130483</td><td>8378447</td></td></tr>
<tr><td>14pipe_14_ooo.cnf</td><td>160242</td><td>11140954</td></td></tr>
<tr><td>15pipe_15_ooo.cnf</td><td>197061</td><td>14821066</td></td></tr>
<tr><td>16pipe_16_ooo.cnf</td><td>239534</td><td>19405933</td></td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>764</td><td>7745</td><td>3472</td><td>1329</td><td>2</td><td>0.069995</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2101</td><td>30706</td><td>26871</td><td>10011</td><td>12</td><td>0.909975</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>4518</td><td>86705</td><td>153024</td><td>52405</td><td>44</td><td>11.845917</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>8269</td><td>196199</td><td>415228</td><td>118901</td><td>84</td><td>51.70384</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>13716</td><td>389931</td><td>1319224</td><td>381483</td><td>235</td><td>416.08776</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo.cnf</td><td>21173</td><td>700461</td><td>3776805</td><td>970692</td><td>508</td><td>2188.59462</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo.cnf</td><td>30965</td><td>1176940</td></td></tr>
<tr><td>9pipe_9_ooo.cnf</td><td>44069</td><td>1904628</td><td>5052554</td><td>755020</td><td>384</td><td>1882.96808</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 15)</td><td colspan=2></td><td>10747178</td><td>2289841</td><td>1269</td><td>4552.180187</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>51461</td><td>2012481</td></td></tr>
<tr><td>11pipe_11_ooo_q0_T0.cnf</td><td>68204</td><td>2909769</td></td></tr>
<tr><td>12pipe_12_ooo_q0_T0.cnf</td><td>89019</td><td>4092323</td></td></tr>
<tr><td>13pipe_13_ooo_q0_T0.cnf</td><td>116489</td><td>5766579</td></td></tr>
<tr><td>14pipe_14_ooo_q0_T0.cnf</td><td>143219</td><td>7488923</td></td></tr>
<tr><td>15pipe_15_ooo_q0_T0.cnf</td><td>176721</td><td>9828736</td></td></tr>
<tr><td>2pipe_2_ooo_q0_T0.cnf</td><td>657</td><td>6046</td><td>3593</td><td>1349</td><td>2</td><td>0.070995</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>1784</td><td>23493</td><td>31710</td><td>10517</td><td>13</td><td>0.850977</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>3823</td><td>65464</td><td>132770</td><td>39507</td><td>30</td><td>6.981929</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td><td>7023</td><td>147630</td><td>334581</td><td>72870</td><td>60</td><td>22.157875</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td><td>11639</td><td>289635</td><td>844607</td><td>175368</td><td>124</td><td>108.18983</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td><td>18358</td><td>516655</td><td>1800918</td><td>362185</td><td>220</td><td>394.90476</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td><td>26906</td><td>856329</td><td>3775265</td><td>731667</td><td>381</td><td>1373.98164</td><td>UNSAT</td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td><td>38499</td><td>1380380</td><td>3155965</td><td>367887</td><td>220</td><td>604.96537</td><td>UNSAT</td></tr>
<tr><td>Total (8 / 14)</td><td colspan=2></td><td>10079409</td><td>1761350</td><td>1050</td><td>2512.103376</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>105929</td><td>8758289</td><td>2917836</td><td>427865</td><td>253</td><td>1440.357</td><td>SAT</td></tr>
<tr><td>12pipe_bug10.cnf</td><td>105929</td><td>8758283</td><td>1813003</td><td>248973</td><td>147</td><td>888.359</td><td>SAT</td></tr>
<tr><td>12pipe_bug2.cnf</td><td>105929</td><td>8758241</td><td>26555</td><td>274</td><td>0</td><td>200.756</td><td>SAT</td></tr>
<tr><td>12pipe_bug3.cnf</td><td>105930</td><td>8758294</td><td>1140027</td><td>126270</td><td>91</td><td>527.273</td><td>SAT</td></tr>
<tr><td>12pipe_bug4.cnf</td><td>105415</td><td>8697049</td><td>752039</td><td>107978</td><td>75</td><td>454.148</td><td>SAT</td></tr>
<tr><td>12pipe_bug5.cnf</td><td>105929</td><td>8758283</td><td>3612427</td><td>683082</td><td>369</td><td>2169.862</td><td>SAT</td></tr>
<tr><td>12pipe_bug6.cnf</td><td>105493</td><td>8597292</td><td>18960</td><td>270</td><td>0</td><td>205.173</td><td>SAT</td></tr>
<tr><td>12pipe_bug7.cnf</td><td>105929</td><td>8758283</td><td>28828</td><td>548</td><td>1</td><td>199.666</td><td>SAT</td></tr>
<tr><td>12pipe_bug8.cnf</td><td>105416</td><td>8714597</td><td>55359</td><td>2085</td><td>3</td><td>200.825</td><td>SAT</td></tr>
<tr><td>12pipe_bug9.cnf</td><td>105928</td><td>8734216</td><td>585036</td><td>70514</td><td>60</td><td>379.222</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>10950070</td><td>1667859</td><td>999</td><td>6665.641</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>81160</td><td>4556496</td><td>830174</td><td>72203</td><td>60</td><td>188.42</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td><td>81164</td><td>4556547</td><td>997949</td><td>104959</td><td>70</td><td>247.415</td><td>SAT</td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>81160</td><td>4556456</td><td>230974</td><td>19687</td><td>20</td><td>68.3909</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>81147</td><td>4556085</td><td>2518734</td><td>276235</td><td>164</td><td>657.2279</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>81194</td><td>4554630</td><td>178975</td><td>15693</td><td>14</td><td>58.3761</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>81160</td><td>4556496</td><td>381461</td><td>32295</td><td>29</td><td>96.8359</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>81184</td><td>4547858</td><td>1174176</td><td>117785</td><td>83</td><td>273.7668</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>81160</td><td>4556496</td><td>2904559</td><td>328496</td><td>191</td><td>755.388</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td><td>81267</td><td>4567469</td><td>4314</td><td>2</td><td>0</td><td>26.66</td><td>SAT</td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>81159</td><td>4553767</td><td>944689</td><td>89415</td><td>62</td><td>214.152</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>10166005</td><td>1056770</td><td>693</td><td>2586.6326</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>679</td><td>6161</td><td>3511</td><td>1385</td><td>2</td><td>0.070995</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>1973</td><td>26217</td><td>25777</td><td>9144</td><td>11</td><td>0.707977</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td><td>4286</td><td>77140</td><td>102329</td><td>32871</td><td>30</td><td>5.698924</td><td>UNSAT</td></tr>
<tr><td>05pipe_k.cnf</td><td>7945</td><td>184641</td><td>292251</td><td>92737</td><td>62</td><td>35.93484</td><td>UNSAT</td></tr>
<tr><td>06pipe_k.cnf</td><td>13501</td><td>400930</td><td>212598</td><td>28776</td><td>29</td><td>12.77265</td><td>UNSAT</td></tr>
<tr><td>07pipe_k.cnf</td><td>20783</td><td>740841</td><td>1534723</td><td>420941</td><td>252</td><td>538.66046</td><td>UNSAT</td></tr>
<tr><td>08pipe_k.cnf</td><td>30665</td><td>1317234</td><td>2454180</td><td>516018</td><td>254</td><td>818.19973</td><td>UNSAT</td></tr>
<tr><td>09pipe_k.cnf</td><td>44203</td><td>2295926</td><td>1358122</td><td>111628</td><td>77</td><td>159.0384</td><td>UNSAT</td></tr>
<tr><td>10pipe_k.cnf</td><td>59700</td><td>3573575</td><td>6254227</td><td>1142643</td><td>510</td><td>3416.9164</td><td>UNSAT</td></tr>
<tr><td>11pipe_k.cnf</td><td>79604</td><td>5548259</td></td></tr>
<tr><td>12pipe_k.cnf</td><td>103708</td><td>8349162</td></td></tr>
<tr><td>13pipe_k.cnf</td><td>132674</td><td>12235539</td></td></tr>
<tr><td>14pipe_k.cnf</td><td>166696</td><td>17522578</td></td></tr>
<tr><td>Total (9 / 13)</td><td colspan=2></td><td>12237718</td><td>2356143</td><td>1227</td><td>4988.000376</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>632</td><td>5838</td><td>3883</td><td>1493</td><td>2</td><td>0.070995</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>1730</td><td>23386</td><td>21121</td><td>7328</td><td>9</td><td>0.530978</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>3685</td><td>65057</td><td>114091</td><td>37336</td><td>30</td><td>6.552932</td><td>UNSAT</td></tr>
<tr><td>05pipe_q0_k.cnf</td><td>6662</td><td>146522</td><td>257183</td><td>65869</td><td>56</td><td>19.141876</td><td>UNSAT</td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>11123</td><td>301392</td><td>211562</td><td>27333</td><td>28</td><td>10.29375</td><td>UNSAT</td></tr>
<tr><td>07pipe_q0_k.cnf</td><td>17101</td><td>514785</td><td>1270899</td><td>259752</td><td>156</td><td>195.41574</td><td>UNSAT</td></tr>
<tr><td>08pipe_q0_k.cnf</td><td>24821</td><td>854130</td><td>2367105</td><td>472785</td><td>254</td><td>601.51557</td><td>UNSAT</td></tr>
<tr><td>09pipe_q0_k.cnf</td><td>35245</td><td>1419287</td><td>1346537</td><td>101484</td><td>68</td><td>103.22897</td><td>UNSAT</td></tr>
<tr><td>10pipe_q0_k.cnf</td><td>46760</td><td>2015434</td><td>5921797</td><td>883919</td><td>474</td><td>1784.26577</td><td>UNSAT</td></tr>
<tr><td>11pipe_q0_k.cnf</td><td>61456</td><td>2916988</td></td></tr>
<tr><td>12pipe_q0_k.cnf</td><td>78914</td><td>4093940</td></td></tr>
<tr><td>13pipe_q0_k.cnf</td><td>100858</td><td>5603534</td></td></tr>
<tr><td>14pipe_q0_k.cnf</td><td>125001</td><td>7497601</td></td></tr>
<tr><td>15pipe_q0_k.cnf</td><td>153042</td><td>9841971</td></td></tr>
<tr><td>Total (9 / 14)</td><td colspan=2></td><td>11514178</td><td>1857299</td><td>1077</td><td>2721.016581</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>200614</td><td>8013212</td><td>1923014</td><td>31312</td><td>29</td><td>107.0841</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug2.cnf</td><td>200536</td><td>8005366</td><td>711711</td><td>1133</td><td>2</td><td>44.2071</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug3.cnf</td><td>200017</td><td>7989548</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug4.cnf</td><td>199855</td><td>7992369</td><td>3896725</td><td>223553</td><td>126</td><td>437.1421</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug5.cnf</td><td>200503</td><td>8005129</td><td>6834344</td><td>409740</td><td>252</td><td>894.6481</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>200509</td><td>8005148</td><td>640534</td><td>2278</td><td>3</td><td>50.4211</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>147176</td><td>5556021</td><td>3630386</td><td>142554</td><td>99</td><td>251.6794</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>194001</td><td>7809939</td><td>1564169</td><td>35683</td><td>30</td><td>109.9811</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td><td>199979</td><td>7992846</td><td>6684032</td><td>426306</td><td>253</td><td>913.3261</td><td>SAT</td></tr>
<tr><td>Total (8 / 9)</td><td colspan=2></td><td>25884915</td><td>1272559</td><td>794</td><td>2808.4891</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>351808</td><td>15494745</td><td>14258587</td><td>825499</td><td>442</td><td>3001.2036</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug10.cnf</td><td>349645</td><td>15436350</td><td>7769522</td><td>311526</td><td>189</td><td>1016.7985</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug2.cnf</td><td>350891</td><td>15458204</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug3.cnf</td><td>351358</td><td>15478358</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug4.cnf</td><td>350323</td><td>15456731</td><td>9662862</td><td>434098</td><td>253</td><td>1439.4845</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug5.cnf</td><td>351797</td><td>15497412</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug6.cnf</td><td>351638</td><td>15480115</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug7.cnf</td><td>351813</td><td>15488558</td><td>867844</td><td>6385</td><td>7</td><td>132.8401</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug8.cnf</td><td>351658</td><td>15485129</td><td>6776641</td><td>283672</td><td>172</td><td>899.5624</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug9.cnf</td><td>391040</td><td>16213645</td><td>10622533</td><td>355031</td><td>218</td><td>1299.1474</td><td>SAT</td></tr>
<tr><td>Total (6 / 10)</td><td colspan=2></td><td>49957989</td><td>2216211</td><td>1281</td><td>7789.0365</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>483468</td><td>13292494</td><td>4517133</td><td>17760</td><td>17</td><td>327.654</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>483455</td><td>13292726</td><td>4501660</td><td>19199</td><td>19</td><td>336.781</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>483458</td><td>13292615</td><td>3143315</td><td>14972</td><td>14</td><td>314.062</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>483334</td><td>13289997</td><td>2056737</td><td>7405</td><td>9</td><td>271.272</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>483003</td><td>13262068</td><td>6104610</td><td>45421</td><td>37</td><td>430.259</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>483133</td><td>13294664</td><td>4125635</td><td>26228</td><td>27</td><td>371.407</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>483476</td><td>13292925</td><td>3075469</td><td>12504</td><td>14</td><td>306.777</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>483436</td><td>13292047</td><td>2349791</td><td>3760</td><td>5</td><td>253.759</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>483451</td><td>13292711</td><td>2435541</td><td>3024</td><td>4</td><td>247.328</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>483460</td><td>13292710</td><td>3657359</td><td>14351</td><td>14</td><td>308.608</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>35967250</td><td>164624</td><td>160</td><td>3167.907</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>16889</td><td>244145</td><td>2669266</td><td>592335</td><td>314</td><td>475.00872</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td><td>32773</td><td>518020</td><td>5980951</td><td>1011625</td><td>509</td><td>1577.24245</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td><td>54024</td><td>933146</td><td>9471420</td><td>1248482</td><td>570</td><td>2285.14598</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq4.cnf</td><td>83095</td><td>1545697</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq5.cnf</td><td>120317</td><td>2391111</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6.cnf</td><td>168000</td><td>3532144</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq7.cnf</td><td>263670</td><td>5951176</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8.cnf</td><td>303312</td><td>6994286</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq9.cnf</td><td>394950</td><td>9444694</td></td></tr>
<tr><td>Total (3 / 9)</td><td colspan=2></td><td>18121637</td><td>2852442</td><td>1393</td><td>4337.39715</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>79699</td><td>1273404</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24_D.cnf</td><td>79529</td><td>1272773</td></td></tr>
<tr><td>Total (0 / 2)</td><td colspan=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>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>84942</td><td>1789068</td><td>5717219</td><td>500275</td><td>254</td><td>608.557</td><td>UNSAT</td></tr>
<tr><td>9vliw_m_9stages_iq1_C1.cnf</td><td>136989</td><td>3193200</td></td></tr>
<tr><td>9vliw_m_9stages_iq2_C1.cnf</td><td>208261</td><td>5218107</td></td></tr>
<tr><td>9vliw_m_9stages_iq3_C1.cnf</td><td>304513</td><td>8056788</td></td></tr>
<tr><td>Total (1 / 4)</td><td colspan=2></td><td>5717219</td><td>500275</td><td>254</td><td>608.557</td><td></td></tr></table><p>