Tinisat 0.22<p>
22 groups, 251 instances, 1-hour cutoff<p>
Instances solved: 183 (78 SAT + 105 UNSAT)<br>
Time: 346002 seconds / 96.11 hours / 4.00 days<br>
Time on solved instances: 101202 seconds (40955 SAT + 60248 UNSAT)<p>
Instances solved in 10 minutes: 124 (12612 seconds)<br>
Instances solved in 15 minutes: 136 (21336 seconds)<br>
Instances solved in 20 minutes: 153 (39164 seconds)<br>
Instances solved in 30 minutes: 164 (56230 seconds)<br>
Instances solved in 60 minutes: 183 (101202 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>31</td><td>/</td><td>32</td><td width=20></td><td>40730.88</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>1733.66</td></tr>
<tr><td>fvp-sat.3.0</td><td width=20></td><td>18</td><td>/</td><td>20</td><td width=20></td><td>3456.35</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>32.8</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>687.88</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>6854.49</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>1001.79</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>62.01</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>826.82</td></tr>
<tr><td>pipe_ooo_unsat_1.0</td><td width=20></td><td>6</td><td>/</td><td>15</td><td width=20></td><td>2498.74</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>3460.08</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>4711.88</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>1857.48</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>8</td><td>/</td><td>13</td><td width=20></td><td>1461</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>10</td><td>/</td><td>14</td><td width=20></td><td>4931.19</td></tr>
<tr><td>vliw_sat_2.0</td><td width=20></td><td>9</td><td>/</td><td>9</td><td width=20></td><td>7422.19</td></tr>
<tr><td>vliw_sat_2.1</td><td width=20></td><td>8</td><td>/</td><td>10</td><td width=20></td><td>10957.48</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>1077.22</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>6788.52</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>649.86</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>5847466</td><td>181117</td><td>125</td><td>662.89</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>276124</td><td>3861235</td><td>6404555</td><td>171727</td><td>123</td><td>686.74</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td><td>292635</td><td>4115946</td><td>7890004</td><td>198941</td><td>126</td><td>841.56</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td><td>309785</td><td>4381995</td><td>7431134</td><td>211632</td><td>126</td><td>925.34</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td><td>327586</td><td>4659661</td><td>8711571</td><td>211672</td><td>126</td><td>1021.28</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td><td>346050</td><td>4949225</td><td>9807995</td><td>205184</td><td>126</td><td>979.78</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td><td>365189</td><td>5250970</td><td>8885035</td><td>214388</td><td>126</td><td>1056.27</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td><td>385015</td><td>5565181</td><td>10349772</td><td>220583</td><td>126</td><td>1157.42</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td><td>405540</td><td>5892145</td><td>11291731</td><td>262524</td><td>157</td><td>1498.08</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td><td>426776</td><td>6232151</td><td>12088524</td><td>239745</td><td>140</td><td>1429.37</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>143519</td><td>1877765</td><td>2227639</td><td>112256</td><td>77</td><td>251.32</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td><td>448735</td><td>6585490</td><td>12454365</td><td>255201</td><td>154</td><td>1550.29</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq53_a.cnf</td><td>471429</td><td>6952455</td><td>12991874</td><td>244193</td><td>141</td><td>1584.36</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq54_a.cnf</td><td>663574</td><td>15489863</td><td>9370438</td><td>285615</td><td>172</td><td>2390.72</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq55_a.cnf</td><td>519070</td><td>7728445</td><td>15426411</td><td>284392</td><td>172</td><td>1973.74</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq56_a.cnf</td><td>544041</td><td>8138066</td><td>19426635</td><td>289127</td><td>176</td><td>2113.13</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq57_a.cnf</td><td>569795</td><td>8562505</td><td>16882321</td><td>263233</td><td>157</td><td>1987.62</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq58_a.cnf</td><td>596344</td><td>9002065</td><td>20617655</td><td>320577</td><td>189</td><td>2524.35</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq59_a.cnf</td><td>623700</td><td>9457051</td><td>20255133</td><td>291138</td><td>179</td><td>2458.94</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq60_a.cnf</td><td>651875</td><td>9927770</td><td>23744452</td><td>334723</td><td>198</td><td>2854.64</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq61_a.cnf</td><td>673311</td><td>10435991</td><td>15227754</td><td>237460</td><td>136</td><td>2027.25</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq34_a.cnf</td><td>154300</td><td>2034001</td><td>2768341</td><td>121595</td><td>86</td><td>287.58</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq62_a.cnf</td><td>710730</td><td>10917645</td><td>24996759</td><td>331292</td><td>195</td><td>3359.67</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq63_a.cnf</td><td>720715</td><td>11606548</td><td>14459582</td><td>186180</td><td>125</td><td>1709.38</td><td>SAT</td></tr>
<tr><td>1dlx_c_iq64_a.cnf</td><td>773005</td><td>11974186</td></td></tr>
<tr><td>1dlx_c_iq35_a.cnf</td><td>165600</td><td>2198895</td><td>3041124</td><td>138393</td><td>93</td><td>348.06</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td><td>228994</td><td>4194027</td><td>2602669</td><td>146891</td><td>103</td><td>471.21</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td><td>245646</td><td>4568332</td><td>2609862</td><td>127285</td><td>92</td><td>445.03</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>202734</td><td>2748125</td><td>4107741</td><td>149099</td><td>106</td><td>467.94</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>216230</td><td>2950261</td><td>4032550</td><td>157286</td><td>111</td><td>493.18</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>230305</td><td>3162370</td><td>4700137</td><td>150071</td><td>107</td><td>521.56</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td><td>244971</td><td>3384721</td><td>5322309</td><td>174136</td><td>124</td><td>652.18</td><td>UNSAT</td></tr>
<tr><td>Total (31 / 32)</td><td colspan=2></td><td>325973538</td><td>6717656</td><td>4194</td><td>40730.88</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>52329</td><td>31728</td><td>29</td><td>11</td><td>UNSAT</td></tr>
<tr><td>engine_4_nd.cnf</td><td>7000</td><td>67586</td><td>138798</td><td>96876</td><td>62</td><td>58.58</td><td>UNSAT</td></tr>
<tr><td>engine_5.cnf</td><td>18788</td><td>214095</td><td>735052</td><td>528924</td><td>261</td><td>1248.94</td><td>UNSAT</td></tr>
<tr><td>engine_5_case1.cnf</td><td>18810</td><td>214185</td><td>20381</td><td>11551</td><td>13</td><td>5.88</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>61112</td><td>38906</td><td>30</td><td>24.25</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>78348</td><td>48742</td><td>40</td><td>59.28</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>278396</td><td>185191</td><td>125</td><td>325.73</td><td>UNSAT</td></tr>
<tr><td>Total (7 / 10)</td><td colspan=2></td><td>1364416</td><td>941918</td><td>560</td><td>1733.66</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>186051</td><td>4973</td><td>6</td><td>4.66</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td><td>35853</td><td>1012271</td></td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>35947</td><td>992674</td><td>82978</td><td>705</td><td>1</td><td>2.53</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>35854</td><td>1012315</td><td>103887</td><td>2595</td><td>4</td><td>3.99</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>3338993</td><td>701997</td><td>379</td><td>622.05</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug07.cnf</td><td>35853</td><td>1012271</td><td>432757</td><td>42510</td><td>33</td><td>18.24</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>35622</td><td>1003074</td><td>411453</td><td>51940</td><td>44</td><td>16.53</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>35726</td><td>1011764</td><td>278772</td><td>27570</td><td>28</td><td>10.05</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>35839</td><td>1012135</td><td>179742</td><td>5625</td><td>6</td><td>4.64</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>35853</td><td>1012271</td><td>740410</td><td>119446</td><td>84</td><td>46.12</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>35854</td><td>1012275</td><td>566178</td><td>81013</td><td>61</td><td>28.81</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>35855</td><td>1012302</td><td>276510</td><td>26523</td><td>27</td><td>9.77</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>35855</td><td>1012407</td><td>91126</td><td>1561</td><td>2</td><td>2.7</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td><td>35853</td><td>1012271</td><td>1361468</td><td>252202</td><td>149</td><td>124.64</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>35853</td><td>1012271</td><td>3435530</td><td>779770</td><td>409</td><td>682.56</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug17.cnf</td><td>35853</td><td>1012271</td><td>4214835</td><td>986460</td><td>509</td><td>1056.92</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug18.cnf</td><td>35853</td><td>1012271</td><td>3041830</td><td>641012</td><td>335</td><td>467.65</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug19.cnf</td><td>35852</td><td>1012266</td><td>791441</td><td>126593</td><td>91</td><td>51.88</td><td>SAT</td></tr>
<tr><td>pipe_64_4_bug20.cnf</td><td>35853</td><td>1012271</td><td>2207264</td><td>456702</td><td>253</td><td>302.61</td><td>SAT</td></tr>
<tr><td>Total (18 / 20)</td><td colspan=2></td><td>21741225</td><td>4309197</td><td>2421</td><td>3456.35</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>2735</td><td>846</td><td>1</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>23785</td><td>5179</td><td>6</td><td>0.36</td><td>UNSAT</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>4583</td><td>41704</td><td>40932</td><td>9799</td><td>12</td><td>1.09</td><td>UNSAT</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>20093</td><td>179492</td><td>613110</td><td>89847</td><td>62</td><td>31.33</td><td>UNSAT</td></tr>
<tr><td>Total (4 / 4)</td><td colspan=2></td><td>680562</td><td>105671</td><td>81</td><td>32.8</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>4650</td><td>1974</td><td>2</td><td>0.06</td><td>UNSAT</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>834</td><td>7026</td><td>3086</td><td>1332</td><td>2</td><td>0.05</td><td>UNSAT</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>925</td><td>8213</td><td>3443</td><td>1297</td><td>2</td><td>0.05</td><td>UNSAT</td></tr>
<tr><td>3pipe.cnf</td><td>2468</td><td>27533</td><td>21216</td><td>7786</td><td>9</td><td>0.54</td><td>UNSAT</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>2223</td><td>26561</td><td>18227</td><td>6730</td><td>8</td><td>0.52</td><td>UNSAT</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>2400</td><td>29981</td><td>28322</td><td>11984</td><td>13</td><td>1.1</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2577</td><td>33270</td><td>30893</td><td>11973</td><td>13</td><td>1.19</td><td>UNSAT</td></tr>
<tr><td>4pipe.cnf</td><td>5237</td><td>80213</td><td>80499</td><td>23177</td><td>23</td><td>4.2</td><td>UNSAT</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>4647</td><td>74554</td><td>64581</td><td>23820</td><td>24</td><td>4.14</td><td>UNSAT</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>4941</td><td>82207</td><td>115529</td><td>45689</td><td>37</td><td>11.43</td><td>UNSAT</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>5233</td><td>89473</td><td>106040</td><td>32431</td><td>29</td><td>7.33</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>5525</td><td>96480</td><td>130312</td><td>37391</td><td>30</td><td>9.84</td><td>UNSAT</td></tr>
<tr><td>5pipe.cnf</td><td>9471</td><td>195452</td><td>102777</td><td>14737</td><td>14</td><td>3.66</td><td>UNSAT</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>8441</td><td>187545</td><td>158892</td><td>44147</td><td>36</td><td>17.66</td><td>UNSAT</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>8851</td><td>201796</td><td>155533</td><td>39086</td><td>30</td><td>14.96</td><td>UNSAT</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>9267</td><td>215440</td><td>162877</td><td>39705</td><td>30</td><td>16.41</td><td>UNSAT</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>9764</td><td>221405</td><td>300064</td><td>72356</td><td>60</td><td>34</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>10113</td><td>240892</td><td>193365</td><td>38991</td><td>30</td><td>17.64</td><td>UNSAT</td></tr>
<tr><td>6pipe.cnf</td><td>15800</td><td>394739</td><td>535690</td><td>109949</td><td>76</td><td>81.9</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>17064</td><td>545612</td><td>649884</td><td>115556</td><td>79</td><td>113.35</td><td>UNSAT</td></tr>
<tr><td>7pipe.cnf</td><td>23910</td><td>751118</td><td>1120524</td><td>198277</td><td>126</td><td>252.56</td><td>UNSAT</td></tr>
<tr><td>7pipe_bug.cnf</td><td>24065</td><td>731850</td><td>596862</td><td>120010</td><td>84</td><td>95.29</td><td>SAT</td></tr>
<tr><td>Total (22 / 22)</td><td colspan=2></td><td>4583266</td><td>998398</td><td>757</td><td>687.88</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>1859994</td><td>295349</td><td>183</td><td>1561.93</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td><td>331848</td><td>5706594</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug7_liveness.cnf</td><td>375775</td><td>6617342</td><td>2019658</td><td>277433</td><td>166</td><td>1753.33</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug8_liveness.cnf</td><td>424320</td><td>7649214</td><td>2606044</td><td>303353</td><td>188</td><td>2087.28</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>103262</td><td>5090</td><td>6</td><td>26.53</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>196655</td><td>3068742</td><td>236996</td><td>11160</td><td>13</td><td>49.14</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>224920</td><td>3596474</td><td>642130</td><td>60578</td><td>51</td><td>261.86</td><td>SAT</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>256697</td><td>4205986</td><td>1625168</td><td>234822</td><td>133</td><td>1114.42</td><td>SAT</td></tr>
<tr><td>Total (7 / 10)</td><td colspan=2></td><td>9093252</td><td>1187785</td><td>740</td><td>6854.49</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>148778</td><td>69967</td><td>60</td><td>36.96</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td><td>24104</td><td>339857</td><td>766184</td><td>400275</td><td>250</td><td>934.26</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>18274</td><td>202528</td><td>120019</td><td>42867</td><td>33</td><td>27.14</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>6128</td><td>65112</td><td>41138</td><td>17254</td><td>16</td><td>3.43</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>1076119</td><td>530363</td><td>359</td><td>1001.79</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>51152</td><td>17153</td><td>16</td><td>3.48</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>14628</td><td>161477</td><td>157719</td><td>57336</td><td>45</td><td>29.42</td><td>UNSAT</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>16011</td><td>210685</td><td>125715</td><td>52353</td><td>44</td><td>29.11</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>334586</td><td>126842</td><td>105</td><td>62.01</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>9243</td><td>4216</td><td>6</td><td>0.42</td><td>SAT</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>3295</td><td>35410</td><td>140516</td><td>88185</td><td>62</td><td>41.12</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>165569</td><td>6547</td><td>7</td><td>15.86</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>3050958</td><td>44822</td><td>36</td><td>769.42</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_no_pe.cnf</td><td>889302</td><td>14582081</td></td></tr>
<tr><td>Total (4 / 6)</td><td colspan=2></td><td>3366286</td><td>143770</td><td>111</td><td>826.82</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>3501</td><td>1379</td><td>2</td><td>0.05</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>2533</td><td>32182</td><td>30544</td><td>11413</td><td>13</td><td>1.01</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>5356</td><td>89506</td><td>153099</td><td>54746</td><td>45</td><td>15.3</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>9705</td><td>200959</td><td>475812</td><td>142738</td><td>99</td><td>80.61</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>15948</td><td>397032</td><td>1255576</td><td>343954</td><td>204</td><td>406.99</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo.cnf</td><td>24415</td><td>711050</td><td>3166217</td><td>814669</td><td>433</td><td>1994.78</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></tr>
<tr><td>Total (6 / 15)</td><td colspan=2></td><td>5084749</td><td>1368899</td><td>796</td><td>2498.74</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>3777</td><td>1339</td><td>2</td><td>0.04</td><td>UNSAT</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>2566</td><td>25625</td><td>31336</td><td>10791</td><td>13</td><td>0.84</td><td>UNSAT</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>5605</td><td>70042</td><td>131102</td><td>40573</td><td>30</td><td>8.16</td><td>UNSAT</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td><td>10482</td><td>156027</td><td>322742</td><td>61844</td><td>52</td><td>21.7</td><td>UNSAT</td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td><td>17710</td><td>304026</td><td>796916</td><td>147700</td><td>104</td><td>99.55</td><td>UNSAT</td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td><td>27846</td><td>538853</td><td>1856774</td><td>357135</td><td>219</td><td>447.43</td><td>UNSAT</td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td><td>41491</td><td>889823</td><td>4051044</td><td>756304</td><td>386</td><td>1696.63</td><td>UNSAT</td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td><td>59024</td><td>1430330</td><td>3937080</td><td>536955</td><td>269</td><td>1185.73</td><td>UNSAT</td></tr>
<tr><td>Total (8 / 14)</td><td colspan=2></td><td>11130771</td><td>1912641</td><td>1075</td><td>3460.08</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>1397488</td><td>148141</td><td>105</td><td>463.47</td><td>SAT</td></tr>
<tr><td>12pipe_bug10.cnf</td><td>118040</td><td>8804672</td><td>2340072</td><td>318328</td><td>189</td><td>1116.41</td><td>SAT</td></tr>
<tr><td>12pipe_bug2.cnf</td><td>118040</td><td>8804630</td><td>204708</td><td>4438</td><td>6</td><td>29.4</td><td>SAT</td></tr>
<tr><td>12pipe_bug3.cnf</td><td>118039</td><td>8804669</td><td>291001</td><td>10757</td><td>13</td><td>50.98</td><td>SAT</td></tr>
<tr><td>12pipe_bug4.cnf</td><td>117504</td><td>8743027</td><td>2142577</td><td>241025</td><td>140</td><td>832.38</td><td>SAT</td></tr>
<tr><td>12pipe_bug5.cnf</td><td>118040</td><td>8804672</td><td>1394725</td><td>116529</td><td>80</td><td>389.15</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>13.81</td><td>SAT</td></tr>
<tr><td>12pipe_bug7.cnf</td><td>118040</td><td>8804672</td><td>2413712</td><td>301217</td><td>187</td><td>1019.63</td><td>SAT</td></tr>
<tr><td>12pipe_bug8.cnf</td><td>117526</td><td>8760516</td><td>138911</td><td>1036</td><td>2</td><td>17.61</td><td>SAT</td></tr>
<tr><td>12pipe_bug9.cnf</td><td>118038</td><td>8780591</td><td>2008007</td><td>249292</td><td>147</td><td>779.04</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>12336678</td><td>1390763</td><td>869</td><td>4711.88</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>179957</td><td>8604</td><td>10</td><td>30.99</td><td>SAT</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td><td>138917</td><td>4678756</td><td>2744840</td><td>277519</td><td>167</td><td>723.96</td><td>SAT</td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>138918</td><td>4678718</td><td>206008</td><td>9165</td><td>11</td><td>31.11</td><td>SAT</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>138917</td><td>4678757</td><td>1607814</td><td>127854</td><td>92</td><td>348.33</td><td>SAT</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>138563</td><td>4675040</td><td>277349</td><td>21085</td><td>21</td><td>58.12</td><td>SAT</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>138918</td><td>4678760</td><td>940023</td><td>64834</td><td>55</td><td>186.12</td><td>SAT</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>138795</td><td>4671352</td><td>289771</td><td>13967</td><td>14</td><td>43.7</td><td>SAT</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>138918</td><td>4678760</td><td>1520862</td><td>131670</td><td>93</td><td>345.02</td><td>SAT</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td><td>138711</td><td>4688614</td><td>65019</td><td>1050</td><td>2</td><td>10.05</td><td>SAT</td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>138916</td><td>4676007</td><td>440883</td><td>27987</td><td>28</td><td>80.08</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>8272526</td><td>683735</td><td>493</td><td>1857.48</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>4337</td><td>1442</td><td>2</td><td>0.04</td><td>UNSAT</td></tr>
<tr><td>03pipe_k.cnf</td><td>2391</td><td>27405</td><td>21542</td><td>6999</td><td>8</td><td>0.49</td><td>UNSAT</td></tr>
<tr><td>04pipe_k.cnf</td><td>5095</td><td>79489</td><td>94194</td><td>27437</td><td>28</td><td>5.75</td><td>UNSAT</td></tr>
<tr><td>05pipe_k.cnf</td><td>9330</td><td>189109</td><td>246625</td><td>65504</td><td>55</td><td>29.33</td><td>UNSAT</td></tr>
<tr><td>06pipe_k.cnf</td><td>15346</td><td>408792</td><td>254611</td><td>27860</td><td>28</td><td>13.08</td><td>UNSAT</td></tr>
<tr><td>07pipe_k.cnf</td><td>23909</td><td>751116</td><td>1278304</td><td>272721</td><td>161</td><td>391.67</td><td>UNSAT</td></tr>
<tr><td>08pipe_k.cnf</td><td>35065</td><td>1332773</td><td>2387017</td><td>422804</td><td>252</td><td>900.66</td><td>UNSAT</td></tr>
<tr><td>09pipe_k.cnf</td><td>49112</td><td>2317839</td><td>1339802</td><td>89705</td><td>62</td><td>119.98</td><td>UNSAT</td></tr>
<tr><td>10pipe_k.cnf</td><td>67300</td><td>3601247</td></td></tr>
<tr><td>11pipe_k.cnf</td><td>89315</td><td>5584003</td></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 (8 / 13)</td><td colspan=2></td><td>5626432</td><td>914472</td><td>596</td><td>1461</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>3286</td><td>1385</td><td>2</td><td>0.04</td><td>UNSAT</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>2476</td><td>25181</td><td>23334</td><td>7383</td><td>9</td><td>0.47</td><td>UNSAT</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>5380</td><td>69072</td><td>98388</td><td>31442</td><td>29</td><td>5.26</td><td>UNSAT</td></tr>
<tr><td>05pipe_q0_k.cnf</td><td>10026</td><td>154409</td><td>266625</td><td>75700</td><td>61</td><td>28.44</td><td>UNSAT</td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>16775</td><td>315960</td><td>228989</td><td>28705</td><td>29</td><td>12.68</td><td>UNSAT</td></tr>
<tr><td>07pipe_q0_k.cnf</td><td>26512</td><td>536414</td><td>1025808</td><td>186804</td><td>125</td><td>141.86</td><td>UNSAT</td></tr>
<tr><td>08pipe_q0_k.cnf</td><td>39434</td><td>887706</td><td>1924584</td><td>293347</td><td>180</td><td>311.4</td><td>UNSAT</td></tr>
<tr><td>09pipe_q0_k.cnf</td><td>55996</td><td>1468197</td><td>1311689</td><td>94425</td><td>62</td><td>108.96</td><td>UNSAT</td></tr>
<tr><td>10pipe_q0_k.cnf</td><td>77639</td><td>2082017</td><td>5750325</td><td>777394</td><td>406</td><td>1696.1</td><td>UNSAT</td></tr>
<tr><td>11pipe_q0_k.cnf</td><td>104244</td><td>3007883</td><td>8237454</td><td>958309</td><td>508</td><td>2625.98</td><td>UNSAT</td></tr>
<tr><td>12pipe_q0_k.cnf</td><td>136800</td><td>4216460</td></td></tr>
<tr><td>13pipe_q0_k.cnf</td><td>176066</td><td>5761591</td></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 (10 / 14)</td><td colspan=2></td><td>18870482</td><td>2454894</td><td>1411</td><td>4931.19</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>8480582</td><td>427402</td><td>253</td><td>1059.85</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug2.cnf</td><td>235928</td><td>8076545</td><td>322730</td><td>82</td><td>0</td><td>16.61</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug3.cnf</td><td>235402</td><td>8060882</td><td>5045911</td><td>203316</td><td>126</td><td>460.85</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug4.cnf</td><td>235277</td><td>8063780</td><td>10683744</td><td>700246</td><td>379</td><td>2013.28</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug5.cnf</td><td>235923</td><td>8076534</td><td>7363397</td><td>410128</td><td>252</td><td>1024.7</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>235926</td><td>8076539</td><td>339729</td><td>2169</td><td>3</td><td>26.99</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>173811</td><td>5609632</td><td>7696410</td><td>504587</td><td>254</td><td>1077.16</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>229942</td><td>7882655</td><td>4251857</td><td>180866</td><td>125</td><td>404.43</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td><td>235184</td><td>8063818</td><td>9031656</td><td>524898</td><td>256</td><td>1338.32</td><td>SAT</td></tr>
<tr><td>Total (9 / 9)</td><td colspan=2></td><td>53216016</td><td>2953694</td><td>1648</td><td>7422.19</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>7732240</td><td>295557</td><td>184</td><td>1023.72</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug10.cnf</td><td>408558</td><td>15554750</td><td>12709694</td><td>569322</td><td>291</td><td>2109.9</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug2.cnf</td><td>409731</td><td>15576332</td><td>10680409</td><td>315294</td><td>189</td><td>1173.89</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug3.cnf</td><td>410219</td><td>15596614</td><td>13816457</td><td>658883</td><td>348</td><td>2469.58</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug4.cnf</td><td>409220</td><td>15574959</td><td>823349</td><td>3413</td><td>5</td><td>75.82</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>1258484</td><td>8518</td><td>10</td><td>90.23</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug8.cnf</td><td>410560</td><td>15603495</td><td>11413051</td><td>587345</td><td>307</td><td>2124.68</td><td>SAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug9.cnf</td><td>449867</td><td>16331249</td><td>14169200</td><td>470619</td><td>254</td><td>1889.66</td><td>SAT</td></tr>
<tr><td>Total (8 / 10)</td><td colspan=2></td><td>72602884</td><td>2908951</td><td>1588</td><td>10957.48</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>4500194</td><td>9194</td><td>11</td><td>103.16</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>521182</td><td>13378625</td><td>6813701</td><td>15345</td><td>14</td><td>158.99</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>521158</td><td>13378532</td><td>4106457</td><td>4602</td><td>6</td><td>83.2</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>521046</td><td>13376161</td><td>3984295</td><td>5587</td><td>6</td><td>79.84</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>520721</td><td>13348117</td><td>5279534</td><td>12602</td><td>14</td><td>122.33</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>520770</td><td>13380350</td><td>4231511</td><td>5649</td><td>6</td><td>94.81</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>521192</td><td>13378781</td><td>5579227</td><td>11085</td><td>13</td><td>118.14</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>521147</td><td>13378010</td><td>3296922</td><td>2504</td><td>3</td><td>52.39</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>521179</td><td>13378617</td><td>9108144</td><td>25810</td><td>27</td><td>210.58</td><td>SAT</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>521187</td><td>13378624</td><td>3833954</td><td>2250</td><td>3</td><td>53.78</td><td>SAT</td></tr>
<tr><td>Total (10 / 10)</td><td colspan=2></td><td>50733939</td><td>94628</td><td>103</td><td>1077.22</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>3122918</td><td>708157</td><td>380</td><td>821.84</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td><td>44095</td><td>542253</td><td>6991613</td><td>1298165</td><td>594</td><td>2478.49</td><td>UNSAT</td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td><td>69789</td><td>968295</td><td>11013971</td><td>1514275</td><td>709</td><td>3488.19</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>21128502</td><td>3520597</td><td>1683</td><td>6788.52</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></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>96177</td><td>1814189</td><td>5854002</td><td>508963</td><td>254</td><td>649.86</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>5854002</td><td>508963</td><td>254</td><td>649.86</td><td></td></tr></table><p>