Tinisat, using restart policy (Luby's, unit=4)<p>
22 groups, 251 instances, 2-hour cutoff<p>
Instances solved: 178 (66 SAT + 112 UNSAT)<br>
Time: 735844 seconds / 204.40 hours / 8.52 days<br>
Time on solved instances: 210244 seconds (82667 SAT + 127577 UNSAT)<p>
Instances solved in 10 minutes: 109 (11833 seconds)<br>
Instances solved in 15 minutes: 116 (16962 seconds)<br>
Instances solved in 20 minutes: 127 (28356 seconds)<br>
Instances solved in 30 minutes: 136 (42272 seconds)<br>
Instances solved in 60 minutes: 154 (90712 seconds)<br>
Instances solved in 90 minutes: 173 (177325 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>86154.14</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>3664.15</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>17552.73</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>47.78</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>447.5</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>13303.54</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>1677.66</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>82.37</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>217.25</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>7328.97</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>2724.88</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>9217.43</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>2676.76</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>11</td><td>/</td><td>13</td><td width=20></td><td>9872.39</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>12459.14</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>16141.22</td></tr>
<tr><td>vliw_sat_2.1</td><td width=20></td><td>3</td><td>/</td><td>10</td><td width=20></td><td>11286.13</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>2711.5</td></tr>
<tr><td>vliw_unsat_2.0</td><td width=20></td><td>2</td><td>/</td><td>9</td><td width=20></td><td>5368.53</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>5881.6</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>1427.99</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>6362283</td><td>163122</td><td>7164</td><td>1191.66</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>276124</td><td>3861235</td><td>6714527</td><td>176854</td><td>7930</td><td>1371.75</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td><td>292635</td><td>4115946</td><td>7164995</td><td>172751</td><td>7675</td><td>1423.89</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td><td>309785</td><td>4381995</td><td>7849744</td><td>178679</td><td>8056</td><td>1593.19</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td><td>327586</td><td>4659661</td><td>8517575</td><td>203191</td><td>8190</td><td>1786.73</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td><td>346050</td><td>4949225</td><td>9332078</td><td>195117</td><td>8189</td><td>1873.60</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td><td>365189</td><td>5250970</td><td>9752625</td><td>208122</td><td>8190</td><td>1998.92</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td><td>385015</td><td>5565181</td><td>10853137</td><td>217826</td><td>8508</td><td>2187.74</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td><td>405540</td><td>5892145</td><td>11978634</td><td>229565</td><td>9209</td><td>2411.63</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td><td>426776</td><td>6232151</td><td>12862759</td><td>231505</td><td>9213</td><td>2588.64</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>143519</td><td>1877765</td><td>2616452</td><td>103823</td><td>4475</td><td>441.80</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td><td>448735</td><td>6585490</td><td>14174936</td><td>270501</td><td>11001</td><td>3168.52</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq53_a.cnf</td><td>471429</td><td>6952455</td><td>13635330</td><td>260095</td><td>10394</td><td>3222.33</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq54_a.cnf</td><td>663574</td><td>15489863</td><td>14122036</td><td>285800</td><td>11767</td><td>5041.95</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq55_a.cnf</td><td>519070</td><td>7728445</td><td>16161006</td><td>266459</td><td>10748</td><td>3505.36</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq56_a.cnf</td><td>544041</td><td>8138066</td><td>17493242</td><td>278643</td><td>11275</td><td>3871.49</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq57_a.cnf</td><td>569795</td><td>8562505</td><td>18629689</td><td>288021</td><td>11802</td><td>4298.92</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq58_a.cnf</td><td>596344</td><td>9002065</td><td>19221275</td><td>306797</td><td>12285</td><td>4702.21</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq59_a.cnf</td><td>623700</td><td>9457051</td><td>21521382</td><td>298710</td><td>12283</td><td>4835.46</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq60_a.cnf</td><td>651875</td><td>9927770</td><td>21232974</td><td>322352</td><td>12930</td><td>5388.82</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq61_a.cnf</td><td>673311</td><td>10435991</td><td>17143729</td><td>255505</td><td>10237</td><td>4448.93</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq34_a.cnf</td><td>154300</td><td>2034001</td><td>2998806</td><td>110410</td><td>4829</td><td>497.50</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq62_a.cnf</td><td>710730</td><td>10917645</td><td>24087334</td><td>341798</td><td>13889</td><td>6054.83</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq63_a.cnf</td><td>720715</td><td>11606548</td><td>18663430</td><td>273421</td><td>11161</td><td>5143.98</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq64_a.cnf</td><td>773005</td><td>11974186</td><td>27807975</td><td>357459</td><td>14430</td><td>6876.32</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq35_a.cnf</td><td>165600</td><td>2198895</td><td>3172822</td><td>112181</td><td>4921</td><td>538.89</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td><td>228994</td><td>4194027</td><td>3834387</td><td>130789</td><td>5848</td><td>905.06</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td><td>245646</td><td>4568332</td><td>3972556</td><td>138281</td><td>6140</td><td>1011.35</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>202734</td><td>2748125</td><td>4434569</td><td>132621</td><td>5942</td><td>789.42</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>216230</td><td>2950261</td><td>4946050</td><td>139329</td><td>6141</td><td>872.19</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>230305</td><td>3162370</td><td>5192778</td><td>149728</td><td>6575</td><td>989.57</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td><td>244971</td><td>3384721</td><td>5951165</td><td>158333</td><td>7034</td><td>1121.49</td><td>UNSAT</td></tr>
<tr><td>Total (32 / 32)</td><td colspan=2></td><td>372402280</td><td>6957788</td><td>288431</td><td>86154.14</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>68319</td><td>34205</td><td>1833</td><td>18.60</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>7000</td><td>67586</td><td>198542</td><td>111471</td><td>4860</td><td>109.12</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td><td>18788</td><td>214095</td><td>1119722</td><td>653337</td><td>24572</td><td>2783.92</td><td>UNSAT</td></tr>
<tr><td>engine_5_case1.cnf</td><td>18810</td><td>214185</td><td>23674</td><td>12203</td><td>746</td><td>10.85</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>74151</td><td>41785</td><td>2046</td><td>43.81</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>87557</td><td>48967</td><td>2301</td><td>99.64</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>338268</td><td>207188</td><td>8190</td><td>598.21</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 10)</td><td colspan=2></td><td>1910233</td><td>1109156</td><td>44548</td><td>3664.15</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>33062</td><td>16</td><td>3</td><td>2.08</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td><td>35853</td><td>1012271</td><td>16589335</td><td>1057667</td><td>36347</td><td>3819.00</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>35947</td><td>992674</td><td>331843</td><td>1038</td><td>93</td><td>5.22</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>35854</td><td>1012315</td><td>452959</td><td>2518</td><td>189</td><td>7.67</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></tr>
<tr><td>pipe_64_4_bug07.cnf</td><td>35853</td><td>1012271</td><td>15201860</td><td>979447</td><td>32766</td><td>3138.99</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>35622</td><td>1003074</td><td>10695</td><td>12</td><td>2</td><td>2.03</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>35726</td><td>1011764</td><td>345448</td><td>470</td><td>50</td><td>3.79</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>35839</td><td>1012135</td><td>15153</td><td>13</td><td>2</td><td>2.04</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>35853</td><td>1012271</td><td>13640095</td><td>901470</td><td>32765</td><td>3086.01</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>35854</td><td>1012275</td><td>3511958</td><td>140047</td><td>6141</td><td>186.04</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>35855</td><td>1012302</td><td>3362588</td><td>139752</td><td>6141</td><td>176.82</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>35855</td><td>1012407</td><td>14896</td><td>14</td><td>2</td><td>2.00</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td><td>35853</td><td>1012271</td></td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>35853</td><td>1012271</td></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>21962410</td><td>1706485</td><td>59832</td><td>7121.04</td><td>SAT</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></tr>
<tr><td>Total (13 / 20)</td><td colspan=2></td><td>75472302</td><td>4928949</td><td>174333</td><td>17552.73</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>2542</td><td>640</td><td>61</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>22862</td><td>4663</td><td>315</td><td>0.48</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>4583</td><td>41704</td><td>37463</td><td>8930</td><td>510</td><td>1.34</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>20093</td><td>179492</td><td>537792</td><td>75660</td><td>3661</td><td>45.94</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td colspan=2></td><td>600659</td><td>89893</td><td>4547</td><td>47.78</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>4019</td><td>1246</td><td>114</td><td>0.06</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>834</td><td>7026</td><td>3592</td><td>1266</td><td>116</td><td>0.06</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>925</td><td>8213</td><td>3913</td><td>1343</td><td>123</td><td>0.07</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>2468</td><td>27533</td><td>25732</td><td>6008</td><td>396</td><td>0.66</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>2223</td><td>26561</td><td>16807</td><td>5274</td><td>362</td><td>0.56</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>2400</td><td>29981</td><td>27805</td><td>9222</td><td>512</td><td>1.14</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2577</td><td>33270</td><td>26728</td><td>7295</td><td>506</td><td>0.99</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>5237</td><td>80213</td><td>91119</td><td>17748</td><td>1021</td><td>4.87</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>4647</td><td>74554</td><td>61687</td><td>17202</td><td>1020</td><td>4.49</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>4941</td><td>82207</td><td>79576</td><td>22360</td><td>1163</td><td>6.48</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>5233</td><td>89473</td><td>85783</td><td>20096</td><td>1022</td><td>6.47</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>5525</td><td>96480</td><td>100856</td><td>23466</td><td>1258</td><td>7.69</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>9471</td><td>195452</td><td>149454</td><td>10678</td><td>636</td><td>4.79</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>8441</td><td>187545</td><td>130094</td><td>30694</td><td>1626</td><td>15.32</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>8851</td><td>201796</td><td>139918</td><td>31202</td><td>1659</td><td>16.19</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>9267</td><td>215440</td><td>144710</td><td>27843</td><td>1530</td><td>16.14</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>9764</td><td>221405</td><td>271851</td><td>57104</td><td>2778</td><td>38.00</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>10113</td><td>240892</td><td>149869</td><td>26783</td><td>1449</td><td>17.09</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td><td>15800</td><td>394739</td><td>523682</td><td>68608</td><td>3315</td><td>63.52</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>17064</td><td>545612</td><td>448687</td><td>67427</td><td>3211</td><td>77.17</td><td>UNSAT</td></tr>
<tr><td>7pipe.cnf</td><td>23910</td><td>751118</td><td>975883</td><td>101896</td><td>4349</td><td>151.44</td><td>UNSAT</td></tr>
<tr><td>7pipe_bug.cnf</td><td>24065</td><td>731850</td><td>201008</td><td>13378</td><td>776</td><td>14.30</td><td>SAT</td></tr>
<tr><td>Total (22 / 22)</td><td colspan=2></td><td>3662773</td><td>568139</td><td>28942</td><td>447.5</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>2081546</td><td>342596</td><td>13946</td><td>3540.12</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td><td>331848</td><td>5706594</td><td>2179134</td><td>360083</td><td>14587</td><td>4025.32</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>1943491</td><td>294696</td><td>12247</td><td>3746.08</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>429917</td><td>56059</td><td>2684</td><td>355.84</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>196655</td><td>3068742</td><td>596140</td><td>76383</td><td>3707</td><td>548.87</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>224920</td><td>3596474</td><td>570894</td><td>68811</td><td>3322</td><td>552.75</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>256697</td><td>4205986</td><td>537239</td><td>61659</td><td>3065</td><td>534.56</td><td>SAT</td></tr>
<tr><td>Total (7 / 10)</td><td colspan=2></td><td>8338361</td><td>1260287</td><td>53558</td><td>13303.54</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>158857</td><td>58182</td><td>2812</td><td>41.16</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td><td>24104</td><td>339857</td><td>1004906</td><td>447379</td><td>16382</td><td>1587.10</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>18274</td><td>202528</td><td>138688</td><td>49457</td><td>2332</td><td>44.42</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>6128</td><td>65112</td><td>46560</td><td>17624</td><td>1021</td><td>4.98</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>1349011</td><td>572642</td><td>22547</td><td>1677.66</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>56424</td><td>15943</td><td>967</td><td>4.87</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>14628</td><td>161477</td><td>176436</td><td>59505</td><td>2914</td><td>43.48</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>16011</td><td>210685</td><td>125132</td><td>43631</td><td>2046</td><td>34.02</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>357992</td><td>119079</td><td>5927</td><td>82.37</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>4973</td><td>833</td><td>73</td><td>0.15</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>3295</td><td>35410</td><td>149314</td><td>77566</td><td>3800</td><td>46.67</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>334444</td><td>55210</td><td>2642</td><td>170.43</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>488731</td><td>133609</td><td>6515</td><td>217.25</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>3924</td><td>1357</td><td>124</td><td>0.07</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2533</td><td>32182</td><td>36150</td><td>11828</td><td>708</td><td>1.67</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>5356</td><td>89506</td><td>154224</td><td>47664</td><td>2243</td><td>18.28</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>9705</td><td>200959</td><td>412401</td><td>105318</td><td>4577</td><td>78.33</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>15948</td><td>397032</td><td>1318086</td><td>363283</td><td>14808</td><td>664.21</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo.cnf</td><td>24415</td><td>711050</td><td>2508503</td><td>633639</td><td>24192</td><td>1772.49</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>4966854</td><td>1050760</td><td>36006</td><td>4793.92</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 15)</td><td colspan=2></td><td>9400142</td><td>2213849</td><td>82658</td><td>7328.97</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>4281</td><td>1307</td><td>122</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>30802</td><td>9064</td><td>510</td><td>0.95</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>5605</td><td>70042</td><td>112382</td><td>23162</td><td>1227</td><td>5.59</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td><td>10482</td><td>156027</td><td>320206</td><td>54234</td><td>2557</td><td>26.29</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td><td>17710</td><td>304026</td><td>733637</td><td>106752</td><td>4605</td><td>88.32</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td><td>27846</td><td>538853</td><td>1753524</td><td>260137</td><td>10395</td><td>380.12</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td><td>41491</td><td>889823</td><td>3547643</td><td>439381</td><td>16382</td><td>995.03</td><td>UNSAT</td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td><td>59024</td><td>1430330</td><td>3476358</td><td>463853</td><td>16730</td><td>1228.53</td><td>UNSAT</td></tr>
<tr><td>Total (8 / 14)</td><td colspan=2></td><td>9978833</td><td>1357890</td><td>52528</td><td>2724.88</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>2850791</td><td>322085</td><td>12923</td><td>2332.42</td><td>SAT</td></tr>
<tr><td>12pipe_bug10.cnf</td><td>118040</td><td>8804672</td><td>1339863</td><td>136280</td><td>6139</td><td>932.63</td><td>SAT</td></tr>
<tr><td>12pipe_bug2.cnf</td><td>118040</td><td>8804630</td><td>333912</td><td>24697</td><td>1292</td><td>202.81</td><td>SAT</td></tr>
<tr><td>12pipe_bug3.cnf</td><td>118039</td><td>8804669</td><td>1147100</td><td>111724</td><td>4875</td><td>762.75</td><td>SAT</td></tr>
<tr><td>12pipe_bug4.cnf</td><td>117504</td><td>8743027</td><td>230725</td><td>15110</td><td>894</td><td>137.55</td><td>SAT</td></tr>
<tr><td>12pipe_bug5.cnf</td><td>118040</td><td>8804672</td><td>2147939</td><td>243671</td><td>9816</td><td>1723.73</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.19</td><td>SAT</td></tr>
<tr><td>12pipe_bug7.cnf</td><td>118040</td><td>8804672</td><td>2444005</td><td>288904</td><td>11878</td><td>2110.06</td><td>SAT</td></tr>
<tr><td>12pipe_bug8.cnf</td><td>117526</td><td>8760516</td><td>19198</td><td>8</td><td>2</td><td>17.08</td><td>SAT</td></tr>
<tr><td>12pipe_bug9.cnf</td><td>118038</td><td>8780591</td><td>1404182</td><td>143502</td><td>6159</td><td>982.21</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>11923192</td><td>1285981</td><td>53978</td><td>9217.43</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>67234</td><td>1252</td><td>115</td><td>17.69</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td><td>138917</td><td>4678756</td><td>1273557</td><td>80974</td><td>3996</td><td>534.72</td><td>SAT</td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>138918</td><td>4678718</td><td>202428</td><td>10461</td><td>625</td><td>69.84</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>138917</td><td>4678757</td><td>1517214</td><td>109649</td><td>4767</td><td>663.49</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>138563</td><td>4675040</td><td>151172</td><td>5532</td><td>380</td><td>42.54</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>138918</td><td>4678760</td><td>1129406</td><td>71066</td><td>3450</td><td>461.07</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>138795</td><td>4671352</td><td>110556</td><td>2968</td><td>234</td><td>28.36</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>138918</td><td>4678760</td><td>342637</td><td>17007</td><td>1020</td><td>118.29</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td><td>138711</td><td>4688614</td><td>72696</td><td>562</td><td>60</td><td>12.01</td><td>SAT</td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>138916</td><td>4676007</td><td>1634101</td><td>117746</td><td>5117</td><td>728.75</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>6501001</td><td>417217</td><td>19764</td><td>2676.76</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>3565</td><td>1237</td><td>113</td><td>0.06</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>2391</td><td>27405</td><td>23885</td><td>5776</td><td>381</td><td>0.64</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td><td>5095</td><td>79489</td><td>74134</td><td>12942</td><td>765</td><td>3.46</td><td>UNSAT</td></tr>
<tr><td>05pipe_k.cnf</td><td>9330</td><td>189109</td><td>214432</td><td>33368</td><td>1788</td><td>19.12</td><td>UNSAT</td></tr>
<tr><td>06pipe_k.cnf</td><td>15346</td><td>408792</td><td>311257</td><td>17934</td><td>1021</td><td>13.55</td><td>UNSAT</td></tr>
<tr><td>07pipe_k.cnf</td><td>23909</td><td>751116</td><td>899938</td><td>101840</td><td>4348</td><td>145.66</td><td>UNSAT</td></tr>
<tr><td>08pipe_k.cnf</td><td>35065</td><td>1332773</td><td>1700642</td><td>153819</td><td>6767</td><td>340.09</td><td>UNSAT</td></tr>
<tr><td>09pipe_k.cnf</td><td>49112</td><td>2317839</td><td>1899763</td><td>68323</td><td>3289</td><td>161.77</td><td>UNSAT</td></tr>
<tr><td>10pipe_k.cnf</td><td>67300</td><td>3601247</td><td>4552248</td><td>275805</td><td>11259</td><td>1122.56</td><td>UNSAT</td></tr>
<tr><td>11pipe_k.cnf</td><td>89315</td><td>5584003</td><td>7590099</td><td>495876</td><td>18425</td><td>3016.82</td><td>UNSAT</td></tr>
<tr><td>12pipe_k.cnf</td><td>115915</td><td>8395649</td><td>11246098</td><td>627671</td><td>23894</td><td>5048.66</td><td>UNSAT</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 (11 / 13)</td><td colspan=2></td><td>28516061</td><td>1794591</td><td>72050</td><td>9872.39</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>4173</td><td>1368</td><td>124</td><td>0.06</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>2476</td><td>25181</td><td>21347</td><td>5394</td><td>377</td><td>0.49</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>5380</td><td>69072</td><td>90310</td><td>21195</td><td>1085</td><td>4.55</td><td>UNSAT</td></tr>
<tr><td>05pipe_q0_k.cnf</td><td>10026</td><td>154409</td><td>205155</td><td>32055</td><td>1721</td><td>12.06</td><td>UNSAT</td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>16775</td><td>315960</td><td>293167</td><td>18293</td><td>1021</td><td>11.80</td><td>UNSAT</td></tr>
<tr><td>07pipe_q0_k.cnf</td><td>26512</td><td>536414</td><td>863899</td><td>106295</td><td>4604</td><td>102.13</td><td>UNSAT</td></tr>
<tr><td>08pipe_q0_k.cnf</td><td>39434</td><td>887706</td><td>1727133</td><td>205175</td><td>8190</td><td>307.04</td><td>UNSAT</td></tr>
<tr><td>09pipe_q0_k.cnf</td><td>55996</td><td>1468197</td><td>1723792</td><td>60272</td><td>2954</td><td>115.86</td><td>UNSAT</td></tr>
<tr><td>10pipe_q0_k.cnf</td><td>77639</td><td>2082017</td><td>4827460</td><td>398392</td><td>16379</td><td>1079.31</td><td>UNSAT</td></tr>
<tr><td>11pipe_q0_k.cnf</td><td>104244</td><td>3007883</td><td>7649955</td><td>613481</td><td>23200</td><td>2275.45</td><td>UNSAT</td></tr>
<tr><td>12pipe_q0_k.cnf</td><td>136800</td><td>4216460</td><td>11110414</td><td>728644</td><td>27332</td><td>3248.91</td><td>UNSAT</td></tr>
<tr><td>13pipe_q0_k.cnf</td><td>176066</td><td>5761591</td><td>15883789</td><td>986837</td><td>33021</td><td>5301.48</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>44400594</td><td>3177401</td><td>120008</td><td>12459.14</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></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug2.cnf</td><td>235928</td><td>8076545</td><td>123643</td><td>20</td><td>4</td><td>17.67</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug3.cnf</td><td>235402</td><td>8060882</td><td>6752901</td><td>307244</td><td>12285</td><td>1950.66</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug4.cnf</td><td>235277</td><td>8063780</td><td>9660562</td><td>645529</td><td>24571</td><td>4954.04</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug5.cnf</td><td>235923</td><td>8076534</td><td>9359916</td><td>560927</td><td>20732</td><td>3866.17</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>235926</td><td>8076539</td><td>1302437</td><td>5094</td><td>347</td><td>74.33</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>173811</td><td>5609632</td><td>2182296</td><td>43665</td><td>2046</td><td>217.49</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>229942</td><td>7882655</td><td>2390796</td><td>33213</td><td>1787</td><td>244.34</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td><td>235184</td><td>8063818</td><td>10569161</td><td>662575</td><td>24573</td><td>4816.52</td><td>SAT</td></tr>
<tr><td>Total (8 / 9)</td><td colspan=2></td><td>42341712</td><td>2258267</td><td>86345</td><td>16141.22</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>13900225</td><td>666522</td><td>24573</td><td>6985.27</td><td>SAT</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>11082998</td><td>432703</td><td>16382</td><td>4204.52</td><td>SAT</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>1748184</td><td>1006</td><td>92</td><td>96.34</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></tr>
<tr><td>Total (3 / 10)</td><td colspan=2></td><td>26731407</td><td>1100231</td><td>41047</td><td>11286.13</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>4868827</td><td>16635</td><td>1018</td><td>325.25</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>521182</td><td>13378625</td><td>3962322</td><td>3461</td><td>253</td><td>122.86</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>521158</td><td>13378532</td><td>4819197</td><td>10274</td><td>604</td><td>231.50</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>521046</td><td>13376161</td><td>4750485</td><td>6898</td><td>474</td><td>188.63</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>520721</td><td>13348117</td><td>5582970</td><td>10973</td><td>637</td><td>245.07</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>520770</td><td>13380350</td><td>5004612</td><td>12438</td><td>763</td><td>269.50</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>521192</td><td>13378781</td><td>3701531</td><td>10948</td><td>637</td><td>233.38</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>521147</td><td>13378010</td><td>4879791</td><td>8573</td><td>510</td><td>199.42</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>521179</td><td>13378617</td><td>6016290</td><td>43646</td><td>2046</td><td>648.06</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>521187</td><td>13378624</td><td>4266201</td><td>11306</td><td>668</td><td>247.83</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>47852226</td><td>135152</td><td>7610</td><td>2711.5</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>2566123</td><td>549017</td><td>20477</td><td>1063.33</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td><td>44095</td><td>542253</td><td>6370460</td><td>1135105</td><td>39419</td><td>4305.20</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td><td>69789</td><td>968295</td></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 (2 / 9)</td><td colspan=2></td><td>8936583</td><td>1684122</td><td>59896</td><td>5368.53</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>41459584</td><td>1226839</td><td>42590</td><td>5881.60</td><td>UNSAT</td></tr>
<tr><td>Total (1 / 2)</td><td colspan=2></td><td>41459584</td><td>1226839</td><td>42590</td><td>5881.6</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>5791267</td><td>471290</td><td>17146</td><td>1427.99</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>5791267</td><td>471290</td><td>17146</td><td>1427.99</td><td></td></tr></table><p>