TiniSatELite<p>
16 groups, 311 instances, 1-hour cutoff<p>
Instances solved: 289 (142 SAT + 147 UNSAT)<br>
Time: 159780 seconds / 44.38 hours / 1.85 days<br>
Time on solved instances: 80580 seconds (71107 SAT + 9473 UNSAT)<p>
Instances solved in 10 minutes: 248 (15059 seconds)<br>
Instances solved in 15 minutes: 257 (22056 seconds)<br>
Instances solved in 20 minutes: 267 (32508 seconds)<br>
Instances solved in 30 minutes: 276 (46764 seconds)<br>
Instances solved in 60 minutes: 289 (80580 seconds)<br>
<p>Instances solved and time on solved instances by group:<p><table border=0>
<tr><td>IBM_FV_2002_01_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>5016.429774</td></tr>
<tr><td>IBM_FV_2002_03_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>2250.402435</td></tr>
<tr><td>IBM_FV_2002_04_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>3826.948395</td></tr>
<tr><td>IBM_FV_2002_05_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>290.285847</td></tr>
<tr><td>IBM_FV_2002_06_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>350.189496</td></tr>
<tr><td>IBM_FV_2002_07_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>47.014579</td></tr>
<tr><td>IBM_FV_2002_09_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>20.465545</td></tr>
<tr><td>IBM_FV_2004_01</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>1376.059848</td></tr>
<tr><td>IBM_FV_2004_07</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>49.18851</td></tr>
<tr><td>IBM_FV_2004_1_11</td><td width=20></td><td>10</td><td>/</td><td>19</td><td width=20></td><td>2443.411552</td></tr>
<tr><td>IBM_FV_2004_18</td><td width=20></td><td>16</td><td>/</td><td>19</td><td width=20></td><td>14481.923162</td></tr>
<tr><td>IBM_FV_2004_20</td><td width=20></td><td>16</td><td>/</td><td>19</td><td width=20></td><td>14574.10303</td></tr>
<tr><td>IBM_FV_2004_2_14</td><td width=20></td><td>18</td><td>/</td><td>19</td><td width=20></td><td>4077.823174</td></tr>
<tr><td>IBM_FV_2004_23</td><td width=20></td><td>17</td><td>/</td><td>19</td><td width=20></td><td>11471.054443</td></tr>
<tr><td>IBM_FV_2004_26</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>305.09607</td></tr>
<tr><td>IBM_FV_2004_29</td><td width=20></td><td>15</td><td>/</td><td>19</td><td width=20></td><td>19999.178508</td></tr>
</table>
<p>

IBM_FV_2002_01_rule
<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>SAT_dat.k45.cnf</td><td>22677</td><td>163478</td><td>581074</td><td>126485</td><td>91</td><td>75.080863</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>25387</td><td>183208</td><td>941440</td><td>189427</td><td>125</td><td>139.15785</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>28097</td><td>202938</td><td>1243832</td><td>283570</td><td>172</td><td>251.42483</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>30807</td><td>222668</td><td>522630</td><td>91368</td><td>62</td><td>41.95681</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>33517</td><td>242398</td><td>987536</td><td>183775</td><td>125</td><td>111.8498</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>36227</td><td>262128</td><td>1807471</td><td>397121</td><td>249</td><td>390.43678</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>38937</td><td>281858</td><td>1051877</td><td>181565</td><td>125</td><td>93.60076</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>41647</td><td>301588</td><td>3064940</td><td>700347</td><td>379</td><td>998.82875</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>44357</td><td>321318</td><td>3422075</td><td>806186</td><td>426</td><td>1490.99673</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>47067</td><td>341048</td><td>2279769</td><td>447621</td><td>253</td><td>441.44072</td><td>SAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td colspan=5></td><td>0.002999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>49777</td><td>360778</td><td>1612</td><td>15</td><td>0</td><td>2.6647</td><td>SAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>3694</td><td>25290</td><td>399</td><td>217</td><td>0</td><td>0.213975</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>52487</td><td>380508</td><td>3822029</td><td>830337</td><td>443</td><td>934.76169</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>6417</td><td>45098</td><td>3091</td><td>1495</td><td>2</td><td>0.489958</td><td>SAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>9127</td><td>64828</td><td>34892</td><td>9300</td><td>12</td><td>2.802943</td><td>SAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>11837</td><td>84558</td><td>26841</td><td>6147</td><td>7</td><td>1.806929</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>14547</td><td>104288</td><td>217407</td><td>53815</td><td>45</td><td>24.311911</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>17257</td><td>124018</td><td>178819</td><td>36200</td><td>30</td><td>13.534897</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>19967</td><td>143748</td><td>747</td><td>70</td><td>0</td><td>1.065879</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>20188481</td><td>4345061</td><td>2546</td><td>5016.429774</td><td></td></tr></table><p>
IBM_FV_2002_03_rule
<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>SAT_dat.k1.cnf</td><td colspan=5></td><td>0.000999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td colspan=5></td><td>0.046992</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>41433</td><td>264163</td><td>3100304</td><td>722899</td><td>381</td><td>1181.44862</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td colspan=5></td><td>0.078987</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td colspan=5></td><td>0.103984</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td colspan=5></td><td>0.12798</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>8261</td><td>49201</td><td>6756</td><td>1194</td><td>2</td><td>0.876913</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>10632</td><td>64579</td><td>33412</td><td>6074</td><td>6</td><td>2.494894</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>13006</td><td>79988</td><td>39679</td><td>5245</td><td>6</td><td>2.528873</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>15380</td><td>95403</td><td>64364</td><td>8976</td><td>11</td><td>4.090853</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>17732</td><td>110560</td><td>74747</td><td>11145</td><td>13</td><td>4.80583</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>20103</td><td>125923</td><td>113922</td><td>16009</td><td>14</td><td>7.17781</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>22473</td><td>141283</td><td>118477</td><td>15059</td><td>14</td><td>7.40279</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>24843</td><td>156643</td><td>421184</td><td>67989</td><td>59</td><td>35.94476</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>27213</td><td>172002</td><td>912470</td><td>165236</td><td>121</td><td>121.65075</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>29583</td><td>187363</td><td>577170</td><td>98183</td><td>62</td><td>49.85072</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>31953</td><td>202721</td><td>927441</td><td>171909</td><td>123</td><td>104.1777</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>34323</td><td>218080</td><td>1368799</td><td>285777</td><td>172</td><td>248.70768</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>36693</td><td>233443</td><td>1557534</td><td>286281</td><td>172</td><td>285.21366</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>39063</td><td>248802</td><td>1345910</td><td>259687</td><td>156</td><td>193.67164</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>10662169</td><td>2121663</td><td>1312</td><td>2250.402435</td><td></td></tr></table><p>
IBM_FV_2002_04_rule
<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>SAT_dat.k1.cnf</td><td colspan=5></td><td>0.000999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td colspan=5></td><td>0.057991</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>55555</td><td>344434</td><td>2145436</td><td>417022</td><td>252</td><td>854.64952</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>681</td><td>4293</td><td>16</td><td>8</td><td>0</td><td>0.186973</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>2898</td><td>16958</td><td>1188</td><td>547</td><td>1</td><td>0.37395</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>6130</td><td>36846</td><td>4650</td><td>1383</td><td>2</td><td>0.658925</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>9425</td><td>57348</td><td>18706</td><td>3367</td><td>5</td><td>1.221897</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>12720</td><td>77857</td><td>33136</td><td>6906</td><td>8</td><td>2.48487</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>16015</td><td>98364</td><td>65180</td><td>11127</td><td>13</td><td>4.02984</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>19309</td><td>118860</td><td>98867</td><td>14430</td><td>14</td><td>6.37481</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>22604</td><td>139364</td><td>152369</td><td>24356</td><td>24</td><td>9.82878</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>25899</td><td>159883</td><td>223595</td><td>32541</td><td>29</td><td>15.16576</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>29195</td><td>180387</td><td>328141</td><td>57606</td><td>46</td><td>40.99173</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>32489</td><td>200896</td><td>491641</td><td>109277</td><td>76</td><td>85.5667</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>35785</td><td>221400</td><td>516678</td><td>111232</td><td>77</td><td>102.16868</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>39079</td><td>241907</td><td>797671</td><td>177874</td><td>124</td><td>195.86865</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>42375</td><td>262415</td><td>757659</td><td>154200</td><td>108</td><td>129.79662</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>45669</td><td>282917</td><td>801161</td><td>131115</td><td>93</td><td>124.17359</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>48965</td><td>303425</td><td>1461097</td><td>347693</td><td>210</td><td>664.66257</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>52259</td><td>323927</td><td>1574145</td><td>475765</td><td>254</td><td>1588.68554</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>9471336</td><td>2076449</td><td>1336</td><td>3826.948395</td><td></td></tr></table><p>
IBM_FV_2002_05_rule
<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>SAT_dat.k1.cnf</td><td>28</td><td>159</td><td>1</td><td>2</td><td>0</td><td>0.002999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>720</td><td>6209</td><td>219</td><td>105</td><td>0</td><td>0.183973</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>88456</td><td>699488</td><td>376025</td><td>24552</td><td>24</td><td>30.57612</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>1471</td><td>11691</td><td>1008</td><td>490</td><td>0</td><td>0.359951</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>3732</td><td>28910</td><td>2943</td><td>912</td><td>1</td><td>0.615921</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>8588</td><td>66245</td><td>6134</td><td>1587</td><td>2</td><td>1.081873</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>13906</td><td>108341</td><td>5375</td><td>1715</td><td>2</td><td>1.43083</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>19231</td><td>150560</td><td>23127</td><td>3367</td><td>5</td><td>2.81277</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>24556</td><td>192788</td><td>52356</td><td>4397</td><td>6</td><td>4.59272</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>29881</td><td>235010</td><td>47757</td><td>5263</td><td>6</td><td>4.49768</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>35206</td><td>277238</td><td>56497</td><td>6272</td><td>7</td><td>5.10263</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>40531</td><td>319460</td><td>170669</td><td>12199</td><td>13</td><td>12.26758</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>45856</td><td>361688</td><td>245628</td><td>18214</td><td>17</td><td>16.98852</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>51181</td><td>403910</td><td>198623</td><td>12104</td><td>13</td><td>14.61347</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>56506</td><td>446138</td><td>279593</td><td>19023</td><td>19</td><td>21.03042</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>61831</td><td>488360</td><td>174868</td><td>11308</td><td>13</td><td>12.58038</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>67156</td><td>530588</td><td>556913</td><td>37313</td><td>30</td><td>40.78933</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>72481</td><td>572810</td><td>553093</td><td>43053</td><td>34</td><td>42.78828</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>77806</td><td>615038</td><td>636845</td><td>44270</td><td>36</td><td>48.37223</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>83131</td><td>657260</td><td>446819</td><td>28964</td><td>29</td><td>29.59817</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>3834493</td><td>275110</td><td>257</td><td>290.285847</td><td></td></tr></table><p>
IBM_FV_2002_06_rule
<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>SAT_dat.k95.cnf</td><td>52422</td><td>373828</td><td>853677</td><td>135677</td><td>93</td><td>105.74047</td><td>SAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td colspan=5></td><td>0.003999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td colspan=5></td><td>0.074988</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>55422</td><td>395298</td><td>346418</td><td>37870</td><td>30</td><td>30.79544</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>4405</td><td>30245</td><td>425</td><td>98</td><td>0</td><td>0.442943</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>7430</td><td>51918</td><td>1764</td><td>403</td><td>0</td><td>0.755917</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>10422</td><td>73313</td><td>7259</td><td>1229</td><td>2</td><td>1.360884</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>13421</td><td>94717</td><td>24721</td><td>5820</td><td>6</td><td>4.247855</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>16421</td><td>116186</td><td>31764</td><td>5764</td><td>6</td><td>4.19783</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>19422</td><td>137657</td><td>41475</td><td>5937</td><td>6</td><td>4.9388</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>22422</td><td>159128</td><td>73685</td><td>9187</td><td>11</td><td>7.29877</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>25422</td><td>180595</td><td>71988</td><td>11972</td><td>13</td><td>8.20274</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>28421</td><td>202062</td><td>58000</td><td>7133</td><td>8</td><td>6.21571</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>31422</td><td>223537</td><td>150636</td><td>18329</td><td>17</td><td>13.37968</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>34422</td><td>245007</td><td>185459</td><td>21983</td><td>21</td><td>16.71665</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>37421</td><td>266475</td><td>265372</td><td>33660</td><td>30</td><td>26.61762</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>40422</td><td>287946</td><td>289101</td><td>35534</td><td>30</td><td>27.68259</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>43422</td><td>309413</td><td>251954</td><td>29686</td><td>29</td><td>23.27456</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>46422</td><td>330888</td><td>278687</td><td>31117</td><td>29</td><td>25.65554</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>49422</td><td>352350</td><td>430635</td><td>56081</td><td>45</td><td>42.58651</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>3363020</td><td>447480</td><td>376</td><td>350.189496</td><td></td></tr></table><p>
IBM_FV_2002_07_rule
<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>SAT_dat.k1.cnf</td><td>326</td><td>1365</td><td>9764</td><td>1045</td><td>2</td><td>0.035997</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>3939</td><td>17240</td><td>722729</td><td>41887</td><td>32</td><td>7.198974</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.234973</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.163984</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.162982</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.182982</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.180983</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.198981</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.204981</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.21098</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.224979</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.20098</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.199978</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.226977</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.228977</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.226976</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.210975</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.237974</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.240974</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>2296</td><td>10063</td><td>347303</td><td>21057</td><td>21</td><td>2.239972</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>6983947</td><td>421958</td><td>412</td><td>47.014579</td><td></td></tr></table><p>
IBM_FV_2002_09_rule
<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>SAT_dat.k1.cnf</td><td colspan=5></td><td>0.000999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>92</td><td>394</td><td>24</td><td>7</td><td>0</td><td>0.083987</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>34257</td><td>218896</td><td>3795</td><td>42</td><td>0</td><td>2.07376</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td colspan=5></td><td>0.214967</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>2737</td><td>17272</td><td>823</td><td>51</td><td>0</td><td>0.312956</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>4707</td><td>29875</td><td>914</td><td>59</td><td>0</td><td>0.420945</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>6677</td><td>42478</td><td>595</td><td>28</td><td>0</td><td>0.515932</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>8648</td><td>55078</td><td>1449</td><td>46</td><td>0</td><td>0.64592</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td colspan=5></td><td>0.622905</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>12587</td><td>80279</td><td>817</td><td>29</td><td>0</td><td>0.838895</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>14557</td><td>92882</td><td>1955</td><td>53</td><td>0</td><td>0.994883</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>16527</td><td>105485</td><td>1983</td><td>46</td><td>0</td><td>1.095871</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>18497</td><td>118088</td><td>1593</td><td>28</td><td>0</td><td>1.177855</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>20468</td><td>130688</td><td>3996</td><td>48</td><td>0</td><td>1.32285</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>22437</td><td>143286</td><td>2455</td><td>42</td><td>0</td><td>1.42983</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>24407</td><td>155889</td><td>1535</td><td>29</td><td>0</td><td>1.47482</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>26377</td><td>168492</td><td>3430</td><td>53</td><td>0</td><td>1.68681</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>28347</td><td>181095</td><td>3305</td><td>49</td><td>0</td><td>1.7588</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>30317</td><td>193698</td><td>2576</td><td>28</td><td>0</td><td>1.79979</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>32288</td><td>206298</td><td>6170</td><td>48</td><td>0</td><td>1.99277</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>37415</td><td>686</td><td>0</td><td>20.465545</td><td></td></tr></table><p>
IBM_FV_2004_01
<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>IBM_FV_2004_rule_batch_01_SAT_dat.k10.cnf</td><td>3418</td><td>19648</td><td>205</td><td>122</td><td>0</td><td>0.196976</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k100.cnf</td><td>38933</td><td>236706</td><td>7203</td><td>531</td><td>1</td><td>1.96779</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k15.cnf</td><td>5198</td><td>30697</td><td>5242</td><td>2224</td><td>3</td><td>0.418969</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k20.cnf</td><td>7179</td><td>42837</td><td>700</td><td>134</td><td>0</td><td>0.35196</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k25.cnf</td><td>9161</td><td>54840</td><td>77218</td><td>19959</td><td>20</td><td>5.333949</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k30.cnf</td><td>11149</td><td>67061</td><td>38755</td><td>7236</td><td>9</td><td>1.955941</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k35.cnf</td><td>13134</td><td>79212</td><td>360613</td><td>75681</td><td>61</td><td>34.775929</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k40.cnf</td><td>15119</td><td>91227</td><td>39307</td><td>5427</td><td>6</td><td>2.003918</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k45.cnf</td><td>17104</td><td>103300</td><td>1323</td><td>63</td><td>0</td><td>0.822909</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k50.cnf</td><td>19089</td><td>115535</td><td>315754</td><td>59832</td><td>49</td><td>21.298898</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k55.cnf</td><td>21077</td><td>127586</td><td>832788</td><td>169527</td><td>123</td><td>89.602888</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k60.cnf</td><td>23062</td><td>139588</td><td>235325</td><td>32376</td><td>29</td><td>11.171878</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k65.cnf</td><td>25044</td><td>150957</td><td>1026103</td><td>208027</td><td>126</td><td>123.388866</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k70.cnf</td><td>27029</td><td>163955</td><td>764068</td><td>140045</td><td>95</td><td>70.715857</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k75.cnf</td><td>29014</td><td>176069</td><td>976128</td><td>185167</td><td>125</td><td>102.48184</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k80.cnf</td><td>30993</td><td>188076</td><td>1932548</td><td>399114</td><td>250</td><td>351.81083</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k85.cnf</td><td>32983</td><td>200116</td><td>1168594</td><td>215548</td><td>126</td><td>109.51283</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k90.cnf</td><td>34963</td><td>212546</td><td>2444737</td><td>522313</td><td>254</td><td>446.44581</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k95.cnf</td><td>36953</td><td>224595</td><td>2473</td><td>36</td><td>0</td><td>1.80181</td><td>SAT</td></tr>
<tr><td>Total (19 / 19)</td><td colspan=2></td><td>10229084</td><td>2043362</td><td>1277</td><td>1376.059848</td><td></td></tr></table><p>
IBM_FV_2004_07
<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>IBM_FV_2004_rule_batch_07_SAT_dat.k10.cnf</td><td>4259</td><td>19129</td><td>1057783</td><td>66052</td><td>57</td><td>16.886973</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k100.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.82597</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k15.cnf</td><td>2061</td><td>9266</td><td>260636</td><td>15578</td><td>14</td><td>1.243979</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k20.cnf</td><td>2061</td><td>9266</td><td>282528</td><td>16487</td><td>15</td><td>1.42998</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k25.cnf</td><td>2061</td><td>9266</td><td>359756</td><td>23982</td><td>24</td><td>2.483978</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k30.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.742979</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k35.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.793976</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k40.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.794976</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k45.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.781976</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k50.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.816974</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k55.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.793975</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k60.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.807974</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k65.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.827972</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k70.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.823973</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k75.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.830972</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k80.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.806973</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k85.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.826971</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k90.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.82497</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k95.cnf</td><td>2061</td><td>9266</td><td>312828</td><td>18425</td><td>17</td><td>1.842969</td><td>UNSAT</td></tr>
<tr><td>Total (19 / 19)</td><td colspan=2></td><td>6653123</td><td>398474</td><td>365</td><td>49.18851</td><td></td></tr></table><p>
IBM_FV_2004_1_11
<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>IBM_FV_2004_rule_batch_1_11_SAT_dat.k10.cnf</td><td>4365</td><td>29318</td><td>994</td><td>220</td><td>0</td><td>0.509931</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k100.cnf</td><td>112886</td><td>749833</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k15.cnf</td><td>9987</td><td>66727</td><td>4161</td><td>935</td><td>1</td><td>1.085871</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k20.cnf</td><td>16055</td><td>106919</td><td>8437</td><td>2850</td><td>4</td><td>1.73581</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k25.cnf</td><td>22098</td><td>147036</td><td>62827</td><td>13524</td><td>14</td><td>6.75075</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k30.cnf</td><td>28139</td><td>187153</td><td>158692</td><td>30374</td><td>29</td><td>17.15669</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k35.cnf</td><td>34187</td><td>227490</td><td>457372</td><td>96911</td><td>62</td><td>77.77362</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k40.cnf</td><td>40224</td><td>267307</td><td>495744</td><td>93754</td><td>62</td><td>80.51156</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k45.cnf</td><td>46303</td><td>307819</td><td>844287</td><td>195804</td><td>125</td><td>241.2925</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k50.cnf</td><td>52368</td><td>348264</td><td>1404222</td><td>404862</td><td>251</td><td>885.41444</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k55.cnf</td><td>58369</td><td>387960</td><td>1847266</td><td>479750</td><td>254</td><td>1131.18038</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k60.cnf</td><td>64475</td><td>428347</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k65.cnf</td><td>70539</td><td>468635</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k70.cnf</td><td>76543</td><td>508531</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k75.cnf</td><td>82611</td><td>549118</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k80.cnf</td><td>88695</td><td>588698</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k85.cnf</td><td>94709</td><td>629245</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k90.cnf</td><td>100844</td><td>670191</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k95.cnf</td><td>106909</td><td>710212</td></td></tr>
<tr><td>Total (10 / 19)</td><td colspan=2></td><td>5284002</td><td>1318984</td><td>802</td><td>2443.411552</td><td></td></tr></table><p>
IBM_FV_2004_18
<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>IBM_FV_2004_rule_batch_18_SAT_dat.k10.cnf</td><td>2996</td><td>21695</td><td>530</td><td>263</td><td>0</td><td>0.399946</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k100.cnf</td><td>60236</td><td>435269</td><td>4363612</td><td>919286</td><td>503</td><td>2028.15336</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k15.cnf</td><td>6291</td><td>45431</td><td>16157</td><td>3035</td><td>4</td><td>1.001922</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k20.cnf</td><td>9452</td><td>68325</td><td>75373</td><td>24709</td><td>25</td><td>10.200888</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k25.cnf</td><td>12630</td><td>91051</td><td>203437</td><td>79758</td><td>61</td><td>74.896856</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k30.cnf</td><td>15806</td><td>114159</td><td>394566</td><td>165076</td><td>121</td><td>225.19483</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k35.cnf</td><td>18976</td><td>137124</td><td>553799</td><td>199155</td><td>126</td><td>286.31779</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k40.cnf</td><td>22139</td><td>159876</td><td>592980</td><td>168675</td><td>123</td><td>175.01776</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k45.cnf</td><td>25318</td><td>182604</td><td>852417</td><td>242395</td><td>141</td><td>307.79573</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k50.cnf</td><td>28508</td><td>205952</td><td>1320849</td><td>446811</td><td>253</td><td>936.62169</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k55.cnf</td><td>31682</td><td>228847</td><td>1907532</td><td>649938</td><td>346</td><td>1793.75766</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k60.cnf</td><td>34844</td><td>251826</td><td>1724849</td><td>425751</td><td>252</td><td>687.16363</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k65.cnf</td><td>38023</td><td>274361</td><td>2260330</td><td>660736</td><td>348</td><td>1591.02259</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k70.cnf</td><td>41193</td><td>297809</td><td>2208886</td><td>537475</td><td>269</td><td>1014.44457</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k75.cnf</td><td>44373</td><td>320532</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k80.cnf</td><td>47537</td><td>342949</td><td>3358316</td><td>896781</td><td>481</td><td>2390.60248</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k85.cnf</td><td>50723</td><td>366231</td><td>3888098</td><td>1036221</td><td>509</td><td>2959.33146</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k90.cnf</td><td>53892</td><td>389682</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k95.cnf</td><td>57064</td><td>412401</td></td></tr>
<tr><td>Total (16 / 19)</td><td colspan=2></td><td>23721731</td><td>6456065</td><td>3562</td><td>14481.923162</td><td></td></tr></table><p>
IBM_FV_2004_20
<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>IBM_FV_2004_rule_batch_20_SAT_dat.k10.cnf</td><td>3467</td><td>25263</td><td>469</td><td>231</td><td>0</td><td>0.371952</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k100.cnf</td><td>62785</td><td>455538</td><td>4229120</td><td>1056735</td><td>510</td><td>2635.09333</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k15.cnf</td><td>6712</td><td>48788</td><td>5404</td><td>1658</td><td>2</td><td>0.849919</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k20.cnf</td><td>10016</td><td>72722</td><td>39519</td><td>9063</td><td>11</td><td>3.098887</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k25.cnf</td><td>13287</td><td>96596</td><td>52193</td><td>15266</td><td>14</td><td>6.091852</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k30.cnf</td><td>16612</td><td>120730</td><td>238964</td><td>72885</td><td>60</td><td>50.40582</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k35.cnf</td><td>19884</td><td>144378</td><td>404223</td><td>118037</td><td>83</td><td>106.04878</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k40.cnf</td><td>23203</td><td>168361</td><td>624903</td><td>215306</td><td>126</td><td>347.38675</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k45.cnf</td><td>26472</td><td>192213</td><td>856604</td><td>273797</td><td>163</td><td>427.36971</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k50.cnf</td><td>29772</td><td>216368</td><td>999712</td><td>325650</td><td>189</td><td>550.31768</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k55.cnf</td><td>33060</td><td>240246</td><td>1698849</td><td>577190</td><td>299</td><td>1478.55964</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k60.cnf</td><td>36389</td><td>264593</td><td>1630853</td><td>504790</td><td>254</td><td>1009.23162</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k65.cnf</td><td>39701</td><td>287733</td><td>2156058</td><td>678997</td><td>363</td><td>1721.21458</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k70.cnf</td><td>43002</td><td>312618</td><td>2389107</td><td>789275</td><td>412</td><td>2289.88754</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k75.cnf</td><td>46235</td><td>336145</td><td>2774337</td><td>779822</td><td>409</td><td>2035.4135</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k80.cnf</td><td>49587</td><td>359707</td><td>2862767</td><td>800184</td><td>419</td><td>1912.76147</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k85.cnf</td><td>52823</td><td>383906</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k90.cnf</td><td>56115</td><td>407399</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k95.cnf</td><td>59401</td><td>431515</td></td></tr>
<tr><td>Total (16 / 19)</td><td colspan=2></td><td>20963082</td><td>6218886</td><td>3314</td><td>14574.10303</td><td></td></tr></table><p>
IBM_FV_2004_2_14
<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>IBM_FV_2004_rule_batch_2_14_SAT_dat.k10.cnf</td><td>3401</td><td>20080</td><td>790</td><td>228</td><td>0</td><td>0.281963</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k100.cnf</td><td>65953</td><td>401390</td><td>3174699</td><td>523038</td><td>254</td><td>789.96948</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k15.cnf</td><td>6876</td><td>41252</td><td>9000</td><td>1767</td><td>2</td><td>0.709937</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k20.cnf</td><td>10352</td><td>62387</td><td>27846</td><td>4650</td><td>6</td><td>1.582911</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k25.cnf</td><td>13828</td><td>83540</td><td>61917</td><td>10697</td><td>13</td><td>4.167884</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k30.cnf</td><td>17299</td><td>104701</td><td>117105</td><td>18967</td><td>19</td><td>8.333859</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k35.cnf</td><td>20780</td><td>125978</td><td>195859</td><td>37041</td><td>30</td><td>16.94683</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k40.cnf</td><td>24251</td><td>147183</td><td>230795</td><td>33774</td><td>30</td><td>14.9008</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k45.cnf</td><td>27724</td><td>168347</td><td>307145</td><td>48925</td><td>40</td><td>31.62578</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k50.cnf</td><td>31200</td><td>189352</td><td>582035</td><td>85063</td><td>62</td><td>68.96175</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k55.cnf</td><td>34675</td><td>210679</td><td>467890</td><td>63962</td><td>53</td><td>40.83272</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k60.cnf</td><td>38153</td><td>231919</td><td>1162036</td><td>163339</td><td>118</td><td>179.8117</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k65.cnf</td><td>41628</td><td>252842</td><td>1361630</td><td>181993</td><td>125</td><td>203.81467</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k70.cnf</td><td>45101</td><td>274285</td><td>1161417</td><td>181362</td><td>125</td><td>175.62064</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k75.cnf</td><td>48576</td><td>295460</td><td>1229202</td><td>211912</td><td>126</td><td>238.90762</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k80.cnf</td><td>52052</td><td>316653</td><td>1736585</td><td>305471</td><td>188</td><td>408.03559</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k85.cnf</td><td>55528</td><td>337204</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k90.cnf</td><td>59000</td><td>358662</td><td>3641236</td><td>537376</td><td>269</td><td>1082.46353</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k95.cnf</td><td>62474</td><td>380188</td><td>2556048</td><td>483124</td><td>254</td><td>810.85551</td><td>UNSAT</td></tr>
<tr><td>Total (18 / 19)</td><td colspan=2></td><td>18023235</td><td>2892689</td><td>1714</td><td>4077.823174</td><td></td></tr></table><p>
IBM_FV_2004_23
<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>IBM_FV_2004_rule_batch_23_SAT_dat.k10.cnf</td><td>2543</td><td>18140</td><td>53</td><td>26</td><td>0</td><td>0.398943</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k100.cnf</td><td>71203</td><td>521855</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k15.cnf</td><td>6412</td><td>46220</td><td>4163</td><td>1205</td><td>2</td><td>0.807912</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k20.cnf</td><td>10237</td><td>74181</td><td>24277</td><td>7054</td><td>8</td><td>2.696868</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k25.cnf</td><td>14146</td><td>102997</td><td>108701</td><td>33399</td><td>30</td><td>18.11783</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k30.cnf</td><td>17841</td><td>130209</td><td>252331</td><td>95994</td><td>62</td><td>93.81678</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k35.cnf</td><td>21912</td><td>159868</td><td>646054</td><td>229126</td><td>126</td><td>443.97474</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k40.cnf</td><td>25827</td><td>188479</td><td>820308</td><td>295747</td><td>184</td><td>593.6817</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k45.cnf</td><td>29299</td><td>214042</td><td>781036</td><td>159558</td><td>114</td><td>134.80165</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k50.cnf</td><td>33550</td><td>245132</td><td>837280</td><td>135472</td><td>93</td><td>86.97962</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k55.cnf</td><td>37418</td><td>273359</td><td>1277941</td><td>276007</td><td>164</td><td>294.58658</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k60.cnf</td><td>41363</td><td>302410</td><td>1862965</td><td>475848</td><td>254</td><td>790.64354</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k65.cnf</td><td>45241</td><td>330328</td><td>2163519</td><td>446105</td><td>253</td><td>645.56148</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k70.cnf</td><td>49135</td><td>358998</td><td>2525939</td><td>429687</td><td>253</td><td>549.41745</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k75.cnf</td><td>53027</td><td>387939</td><td>3356338</td><td>710835</td><td>380</td><td>1423.65541</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k80.cnf</td><td>55987</td><td>409919</td><td>3843119</td><td>769052</td><td>396</td><td>1375.31534</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k85.cnf</td><td>60784</td><td>443918</td><td>4348763</td><td>908751</td><td>490</td><td>2025.71632</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k90.cnf</td><td>64657</td><td>473078</td><td>5359040</td><td>1158130</td><td>510</td><td>2990.88228</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k95.cnf</td><td>68546</td><td>501393</td></td></tr>
<tr><td>Total (17 / 19)</td><td colspan=2></td><td>28211827</td><td>6131996</td><td>3319</td><td>11471.054443</td><td></td></tr></table><p>
IBM_FV_2004_26
<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>IBM_FV_2004_rule_batch_26_SAT_dat.k10.cnf</td><td>28104</td><td>214170</td><td>82657</td><td>640</td><td>1</td><td>4.21161</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k100.cnf</td><td>187870</td><td>1853812</td><td>88886</td><td>327</td><td>0</td><td>29.0799</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k15.cnf</td><td>31470</td><td>287397</td><td>34877</td><td>327</td><td>0</td><td>4.45051</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k20.cnf</td><td>40670</td><td>379771</td><td>38510</td><td>327</td><td>0</td><td>5.83536</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k25.cnf</td><td>49870</td><td>471773</td><td>40416</td><td>327</td><td>0</td><td>7.2452</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k30.cnf</td><td>59070</td><td>563863</td><td>45822</td><td>328</td><td>0</td><td>8.73005</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k35.cnf</td><td>68270</td><td>655701</td><td>46607</td><td>327</td><td>0</td><td>9.98491</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k40.cnf</td><td>77470</td><td>748168</td><td>49667</td><td>329</td><td>0</td><td>11.50174</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k45.cnf</td><td>86670</td><td>840029</td><td>52782</td><td>327</td><td>0</td><td>12.84559</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k50.cnf</td><td>95870</td><td>932535</td><td>59972</td><td>328</td><td>0</td><td>14.4894</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k55.cnf</td><td>105070</td><td>1024098</td><td>60041</td><td>328</td><td>0</td><td>15.9373</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k60.cnf</td><td>114270</td><td>1116942</td><td>62817</td><td>329</td><td>0</td><td>17.3791</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k65.cnf</td><td>123470</td><td>1208389</td><td>66017</td><td>328</td><td>0</td><td>18.637</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k70.cnf</td><td>132670</td><td>1300914</td><td>73979</td><td>327</td><td>0</td><td>20.6818</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k75.cnf</td><td>141870</td><td>1392526</td><td>72089</td><td>326</td><td>0</td><td>21.5557</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k80.cnf</td><td>151070</td><td>1485010</td><td>76059</td><td>329</td><td>0</td><td>23.3844</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k85.cnf</td><td>160270</td><td>1576770</td><td>77600</td><td>327</td><td>0</td><td>24.5713</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k90.cnf</td><td>169470</td><td>1669436</td><td>89874</td><td>327</td><td>0</td><td>26.7212</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k95.cnf</td><td>178670</td><td>1760995</td><td>86210</td><td>329</td><td>0</td><td>27.854</td><td>UNSAT</td></tr>
<tr><td>Total (19 / 19)</td><td colspan=2></td><td>1204882</td><td>6537</td><td>1</td><td>305.09607</td><td></td></tr></table><p>
IBM_FV_2004_29
<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>IBM_FV_2004_rule_batch_29_SAT_dat.k10.cnf</td><td>2605</td><td>16830</td><td>23202</td><td>12569</td><td>14</td><td>2.340981</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k100.cnf</td><td>34191</td><td>234066</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k15.cnf</td><td>4271</td><td>28386</td><td>154185</td><td>82324</td><td>62</td><td>47.829972</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k20.cnf</td><td>6031</td><td>40475</td><td>539763</td><td>292686</td><td>179</td><td>446.298962</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k25.cnf</td><td>7791</td><td>52579</td><td>1498877</td><td>853266</td><td>447</td><td>3275.867951</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k30.cnf</td><td>9551</td><td>64698</td><td>1161588</td><td>525047</td><td>256</td><td>867.329942</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k35.cnf</td><td>11311</td><td>76777</td><td>1170794</td><td>450713</td><td>253</td><td>592.741931</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k40.cnf</td><td>13071</td><td>88878</td><td>1028833</td><td>357926</td><td>219</td><td>364.758921</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k45.cnf</td><td>14831</td><td>100972</td><td>1825557</td><td>664368</td><td>350</td><td>1072.60091</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k50.cnf</td><td>16591</td><td>113113</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k55.cnf</td><td>18351</td><td>125218</td><td>3312620</td><td>1288309</td><td>587</td><td>3407.626891</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k60.cnf</td><td>20111</td><td>137275</td><td>3555881</td><td>1313671</td><td>604</td><td>3233.446878</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k65.cnf</td><td>21871</td><td>149374</td><td>1857634</td><td>540833</td><td>270</td><td>594.859869</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k70.cnf</td><td>23631</td><td>161528</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k75.cnf</td><td>25391</td><td>173633</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k80.cnf</td><td>27151</td><td>185737</td><td>3925649</td><td>1220406</td><td>541</td><td>2630.86284</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k85.cnf</td><td>28911</td><td>197759</td><td>2419304</td><td>602042</td><td>316</td><td>579.06483</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k90.cnf</td><td>30671</td><td>209871</td><td>3089694</td><td>834388</td><td>443</td><td>1090.79282</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k95.cnf</td><td>32431</td><td>222046</td><td>4272998</td><td>1146334</td><td>510</td><td>1792.75481</td><td>SAT</td></tr>
<tr><td>Total (15 / 19)</td><td colspan=2></td><td>29836579</td><td>10184882</td><td>5051</td><td>19999.178508</td><td></td></tr></table><p>