# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:17:08 2006] READ BEGIN : csp/tai_7x7_6.csp [Mon Jun 19 23:17:08 2006] READ END : csp/tai_7x7_6.csp (1 seconds) [Mon Jun 19 23:17:09 2006] READ CPU : 0.65 = 0.65 + 0 + 0 + 0 # BOUND : makespan 451 614 GENERATE_CNF 614 BEGIN : [Mon Jun 19 23:17:09 2006] GENERATE_CNF 614 END : 30986 variables 367026 clauses 7581293 bytes (14 seconds) [Mon Jun 19 23:17:23 2006] GENERATE_CNF 614 CPU : 13.76 = 13.71 + 0.05 + 0 + 0 MODIFY_CNF 532 BEGIN : [Mon Jun 19 23:17:23 2006] MODIFY_CNF 532 END : 7581298 bytes (0 seconds) [Mon Jun 19 23:17:23 2006] MODIFY_CNF 532 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 532 BEGIN : [Mon Jun 19 23:17:23 2006] CMD : minisat /tmp/csp2sat14036.cnf /tmp/csp2sat14036.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 317874 924065 | 105958 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (12 /sec) decisions : 172 (358 /sec) propagations : 45356 (94492 /sec) conflict literals : 48 (5.88 % deleted) Memory used : 17.90 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 532 END : (0 seconds) [Mon Jun 19 23:17:23 2006] VERIFY_CNF 532 CPU : 0.52 = 0 + 0 + 0.5 + 0.02 # RESULT : makespan 532 SATISFIABLE SHOW_RESULT 532 BEGIN : [Mon Jun 19 23:17:23 2006] # ASSIGN : makespan 532 # ASSIGN : s_0_0 162 # ASSIGN : s_0_1 401 # ASSIGN : s_0_2 249 # ASSIGN : s_0_3 42 # ASSIGN : s_0_4 477 # ASSIGN : s_0_5 44 # ASSIGN : s_0_6 64 # ASSIGN : s_1_0 288 # ASSIGN : s_1_1 192 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 377 # ASSIGN : s_1_4 320 # ASSIGN : s_1_5 83 # ASSIGN : s_1_6 152 # ASSIGN : s_2_0 363 # ASSIGN : s_2_1 131 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 300 # ASSIGN : s_2_4 44 # ASSIGN : s_2_5 224 # ASSIGN : s_2_6 199 # ASSIGN : s_3_0 438 # ASSIGN : s_3_1 15 # ASSIGN : s_3_2 79 # ASSIGN : s_3_3 54 # ASSIGN : s_3_4 140 # ASSIGN : s_3_5 319 # ASSIGN : s_3_6 229 # ASSIGN : s_4_0 15 # ASSIGN : s_4_1 486 # ASSIGN : s_4_2 161 # ASSIGN : s_4_3 79 # ASSIGN : s_4_4 236 # ASSIGN : s_4_5 360 # ASSIGN : s_4_6 295 # ASSIGN : s_5_0 21 # ASSIGN : s_5_1 67 # ASSIGN : s_5_2 169 # ASSIGN : s_5_3 472 # ASSIGN : s_5_4 260 # ASSIGN : s_5_5 451 # ASSIGN : s_5_6 354 # ASSIGN : s_6_0 81 # ASSIGN : s_6_1 251 # ASSIGN : s_6_2 344 # ASSIGN : s_6_3 156 # ASSIGN : s_6_4 380 # ASSIGN : s_6_5 456 # ASSIGN : s_6_6 483 SHOW_RESULT 532 END : 532 (0 seconds) [Mon Jun 19 23:17:23 2006] SHOW_RESULT 532 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 451 532 MODIFY_CNF 491 BEGIN : [Mon Jun 19 23:17:23 2006] MODIFY_CNF 491 END : 7581298 bytes (0 seconds) [Mon Jun 19 23:17:23 2006] MODIFY_CNF 491 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 491 BEGIN : [Mon Jun 19 23:17:23 2006] CMD : minisat /tmp/csp2sat14036.cnf /tmp/csp2sat14036.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 293766 851741 | 97922 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (2 /sec) decisions : 106 (216 /sec) propagations : 31446 (64176 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 17.96 MB CPU time : 0.49 s SATISFIABLE VERIFY_CNF 491 END : (1 seconds) [Mon Jun 19 23:17:24 2006] VERIFY_CNF 491 CPU : 0.52 = 0 + 0 + 0.5 + 0.02 # RESULT : makespan 491 SATISFIABLE SHOW_RESULT 491 BEGIN : [Mon Jun 19 23:17:24 2006] # ASSIGN : makespan 491 # ASSIGN : s_0_0 136 # ASSIGN : s_0_1 354 # ASSIGN : s_0_2 223 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 436 # ASSIGN : s_0_5 7 # ASSIGN : s_0_6 40 # ASSIGN : s_1_0 96 # ASSIGN : s_1_1 253 # ASSIGN : s_1_2 318 # ASSIGN : s_1_3 396 # ASSIGN : s_1_4 177 # ASSIGN : s_1_5 27 # ASSIGN : s_1_6 128 # ASSIGN : s_2_0 276 # ASSIGN : s_2_1 430 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 105 # ASSIGN : s_2_4 1 # ASSIGN : s_2_5 195 # ASSIGN : s_2_6 168 # ASSIGN : s_3_0 351 # ASSIGN : s_3_1 312 # ASSIGN : s_3_2 27 # ASSIGN : s_3_3 2 # ASSIGN : s_3_4 88 # ASSIGN : s_3_5 271 # ASSIGN : s_3_6 193 # ASSIGN : s_4_0 13 # ASSIGN : s_4_1 188 # ASSIGN : s_4_2 19 # ASSIGN : s_4_3 28 # ASSIGN : s_4_4 234 # ASSIGN : s_4_5 349 # ASSIGN : s_4_6 259 # ASSIGN : s_5_0 445 # ASSIGN : s_5_1 30 # ASSIGN : s_5_2 104 # ASSIGN : s_5_3 184 # ASSIGN : s_5_4 258 # ASSIGN : s_5_5 440 # ASSIGN : s_5_6 318 # ASSIGN : s_6_0 19 # ASSIGN : s_6_1 94 # ASSIGN : s_6_2 187 # ASSIGN : s_6_3 244 # ASSIGN : s_6_4 339 # ASSIGN : s_6_5 464 # ASSIGN : s_6_6 415 SHOW_RESULT 491 END : 491 (0 seconds) [Mon Jun 19 23:17:24 2006] SHOW_RESULT 491 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 451 491 MODIFY_CNF 471 BEGIN : [Mon Jun 19 23:17:24 2006] MODIFY_CNF 471 END : 7581298 bytes (0 seconds) [Mon Jun 19 23:17:24 2006] MODIFY_CNF 471 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 471 BEGIN : [Mon Jun 19 23:17:24 2006] CMD : minisat /tmp/csp2sat14036.cnf /tmp/csp2sat14036.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 282006 816461 | 94002 0 0 nan | 0.000 % | | 100 | 282006 816461 | 103402 100 2390 23.9 | 32.689 % | | 250 | 282006 816461 | 113742 250 6277 25.1 | 32.689 % | ============================================================================== restarts : 3 conflicts : 295 (276 /sec) decisions : 626 (585 /sec) propagations : 707614 (661321 /sec) conflict literals : 7488 (18.59 % deleted) Memory used : 17.98 MB CPU time : 1.07 s SATISFIABLE VERIFY_CNF 471 END : (1 seconds) [Mon Jun 19 23:17:25 2006] VERIFY_CNF 471 CPU : 1.17 = 0 + 0 + 1.09 + 0.08 # RESULT : makespan 471 SATISFIABLE SHOW_RESULT 471 BEGIN : [Mon Jun 19 23:17:25 2006] # ASSIGN : makespan 471 # ASSIGN : s_0_0 163 # ASSIGN : s_0_1 395 # ASSIGN : s_0_2 300 # ASSIGN : s_0_3 161 # ASSIGN : s_0_4 98 # ASSIGN : s_0_5 280 # ASSIGN : s_0_6 10 # ASSIGN : s_1_0 79 # ASSIGN : s_1_1 111 # ASSIGN : s_1_2 178 # ASSIGN : s_1_3 313 # ASSIGN : s_1_4 256 # ASSIGN : s_1_5 2 # ASSIGN : s_1_6 431 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 241 # ASSIGN : s_2_2 407 # ASSIGN : s_2_3 408 # ASSIGN : s_2_4 320 # ASSIGN : s_2_5 76 # ASSIGN : s_2_6 152 # ASSIGN : s_3_0 250 # ASSIGN : s_3_1 170 # ASSIGN : s_3_2 410 # ASSIGN : s_3_3 136 # ASSIGN : s_3_4 9 # ASSIGN : s_3_5 209 # ASSIGN : s_3_6 344 # ASSIGN : s_4_0 344 # ASSIGN : s_4_1 65 # ASSIGN : s_4_2 57 # ASSIGN : s_4_3 236 # ASSIGN : s_4_4 153 # ASSIGN : s_4_5 380 # ASSIGN : s_4_6 177 # ASSIGN : s_5_0 350 # ASSIGN : s_5_1 1 # ASSIGN : s_5_2 96 # ASSIGN : s_5_3 176 # ASSIGN : s_5_4 411 # ASSIGN : s_5_5 71 # ASSIGN : s_5_6 247 # ASSIGN : s_6_0 396 # ASSIGN : s_6_1 302 # ASSIGN : s_6_2 264 # ASSIGN : s_6_3 8 # ASSIGN : s_6_4 180 # ASSIGN : s_6_5 153 # ASSIGN : s_6_6 103 SHOW_RESULT 471 END : 471 (0 seconds) [Mon Jun 19 23:17:25 2006] SHOW_RESULT 471 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 451 471 MODIFY_CNF 461 BEGIN : [Mon Jun 19 23:17:25 2006] MODIFY_CNF 461 END : 7581298 bytes (0 seconds) [Mon Jun 19 23:17:25 2006] MODIFY_CNF 461 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 461 BEGIN : [Mon Jun 19 23:17:25 2006] CMD : minisat /tmp/csp2sat14036.cnf /tmp/csp2sat14036.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 276126 798821 | 92042 0 0 nan | 0.000 % | | 103 | 276126 798821 | 101246 103 3414 33.1 | 34.303 % | ============================================================================== restarts : 2 conflicts : 163 (201 /sec) decisions : 373 (460 /sec) propagations : 380730 (470037 /sec) conflict literals : 4582 (9.68 % deleted) Memory used : 17.98 MB CPU time : 0.81 s SATISFIABLE VERIFY_CNF 461 END : (1 seconds) [Mon Jun 19 23:17:26 2006] VERIFY_CNF 461 CPU : 0.86 = 0 + 0 + 0.83 + 0.03 # RESULT : makespan 461 SATISFIABLE SHOW_RESULT 461 BEGIN : [Mon Jun 19 23:17:26 2006] # ASSIGN : makespan 461 # ASSIGN : s_0_0 116 # ASSIGN : s_0_1 13 # ASSIGN : s_0_2 311 # ASSIGN : s_0_3 11 # ASSIGN : s_0_4 406 # ASSIGN : s_0_5 291 # ASSIGN : s_0_6 203 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 307 # ASSIGN : s_1_2 229 # ASSIGN : s_1_3 366 # ASSIGN : s_1_4 101 # ASSIGN : s_1_5 32 # ASSIGN : s_1_6 163 # ASSIGN : s_2_0 32 # ASSIGN : s_2_1 246 # ASSIGN : s_2_2 460 # ASSIGN : s_2_3 183 # ASSIGN : s_2_4 319 # ASSIGN : s_2_5 107 # ASSIGN : s_2_6 7 # ASSIGN : s_3_0 204 # ASSIGN : s_3_1 422 # ASSIGN : s_3_2 143 # ASSIGN : s_3_3 97 # ASSIGN : s_3_4 8 # ASSIGN : s_3_5 381 # ASSIGN : s_3_6 298 # ASSIGN : s_4_0 455 # ASSIGN : s_4_1 376 # ASSIGN : s_4_2 447 # ASSIGN : s_4_3 20 # ASSIGN : s_4_4 158 # ASSIGN : s_4_5 200 # ASSIGN : s_4_6 99 # ASSIGN : s_5_0 318 # ASSIGN : s_5_1 182 # ASSIGN : s_5_2 42 # ASSIGN : s_5_3 122 # ASSIGN : s_5_4 258 # ASSIGN : s_5_5 27 # ASSIGN : s_5_6 364 # ASSIGN : s_6_0 380 # ASSIGN : s_6_1 89 # ASSIGN : s_6_2 4 # ASSIGN : s_6_3 258 # ASSIGN : s_6_4 182 # ASSIGN : s_6_5 353 # ASSIGN : s_6_6 40 SHOW_RESULT 461 END : 461 (0 seconds) [Mon Jun 19 23:17:26 2006] SHOW_RESULT 461 CPU : 0.0400000000000009 = 0.0400000000000009 + 0 + 0 + 0 # BOUND : makespan 451 461 MODIFY_CNF 456 BEGIN : [Mon Jun 19 23:17:26 2006] MODIFY_CNF 456 END : 7581297 bytes (0 seconds) [Mon Jun 19 23:17:26 2006] MODIFY_CNF 456 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 456 BEGIN : [Mon Jun 19 23:17:26 2006] CMD : minisat /tmp/csp2sat14036.cnf /tmp/csp2sat14036.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 273186 790001 | 91062 0 0 nan | 0.000 % | | 100 | 273186 790001 | 100168 100 2163 21.6 | 35.109 % | | 250 | 273186 790001 | 110185 250 6573 26.3 | 35.109 % | ============================================================================== restarts : 3 conflicts : 332 (270 /sec) decisions : 589 (479 /sec) propagations : 829021 (674001 /sec) conflict literals : 8952 (14.90 % deleted) Memory used : 17.98 MB CPU time : 1.23 s SATISFIABLE VERIFY_CNF 456 END : (1 seconds) [Mon Jun 19 23:17:27 2006] VERIFY_CNF 456 CPU : 1.31 = 0 + 0 + 1.24 + 0.07 # RESULT : makespan 456 SATISFIABLE SHOW_RESULT 456 BEGIN : [Mon Jun 19 23:17:27 2006] # ASSIGN : makespan 456 # ASSIGN : s_0_0 3 # ASSIGN : s_0_1 380 # ASSIGN : s_0_2 211 # ASSIGN : s_0_3 121 # ASSIGN : s_0_4 312 # ASSIGN : s_0_5 101 # ASSIGN : s_0_6 123 # ASSIGN : s_1_0 424 # ASSIGN : s_1_1 321 # ASSIGN : s_1_2 108 # ASSIGN : s_1_3 13 # ASSIGN : s_1_4 255 # ASSIGN : s_1_5 186 # ASSIGN : s_1_6 384 # ASSIGN : s_2_0 349 # ASSIGN : s_2_1 260 # ASSIGN : s_2_2 195 # ASSIGN : s_2_3 196 # ASSIGN : s_2_4 92 # ASSIGN : s_2_5 16 # ASSIGN : s_2_6 431 # ASSIGN : s_3_0 165 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 306 # ASSIGN : s_3_3 259 # ASSIGN : s_3_4 367 # ASSIGN : s_3_5 124 # ASSIGN : s_3_6 57 # ASSIGN : s_4_0 159 # ASSIGN : s_4_1 40 # ASSIGN : s_4_2 203 # ASSIGN : s_4_3 284 # ASSIGN : s_4_4 6 # ASSIGN : s_4_5 365 # ASSIGN : s_4_6 220 # ASSIGN : s_5_0 90 # ASSIGN : s_5_1 196 # ASSIGN : s_5_2 376 # ASSIGN : s_5_3 136 # ASSIGN : s_5_4 30 # ASSIGN : s_5_5 274 # ASSIGN : s_5_6 279 # ASSIGN : s_6_0 259 # ASSIGN : s_6_1 86 # ASSIGN : s_6_2 50 # ASSIGN : s_6_3 361 # ASSIGN : s_6_4 179 # ASSIGN : s_6_5 334 # ASSIGN : s_6_6 1 SHOW_RESULT 456 END : 456 (0 seconds) [Mon Jun 19 23:17:27 2006] SHOW_RESULT 456 CPU : 0.0499999999999989 = 0.0499999999999989 + 0 + 0 + 0 # BOUND : makespan 451 456 MODIFY_CNF 453 BEGIN : [Mon Jun 19 23:17:27 2006] MODIFY_CNF 453 END : 7581297 bytes (0 seconds) [Mon Jun 19 23:17:27 2006] MODIFY_CNF 453 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 453 BEGIN : [Mon Jun 19 23:17:27 2006] CMD : minisat /tmp/csp2sat14036.cnf /tmp/csp2sat14036.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 271422 784709 | 90474 0 0 nan | 0.000 % | | 100 | 271422 784709 | 99521 100 3067 30.7 | 35.594 % | ============================================================================== restarts : 2 conflicts : 151 (191 /sec) decisions : 289 (366 /sec) propagations : 380445 (481576 /sec) conflict literals : 4494 (11.88 % deleted) Memory used : 17.98 MB CPU time : 0.79 s SATISFIABLE VERIFY_CNF 453 END : (1 seconds) [Mon Jun 19 23:17:28 2006] VERIFY_CNF 453 CPU : 0.86 = 0 + 0 + 0.8 + 0.06 # RESULT : makespan 453 SATISFIABLE SHOW_RESULT 453 BEGIN : [Mon Jun 19 23:17:28 2006] # ASSIGN : makespan 453 # ASSIGN : s_0_0 360 # ASSIGN : s_0_1 123 # ASSIGN : s_0_2 8 # ASSIGN : s_0_3 451 # ASSIGN : s_0_4 287 # ASSIGN : s_0_5 103 # ASSIGN : s_0_6 199 # ASSIGN : s_1_0 59 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 197 # ASSIGN : s_1_3 275 # ASSIGN : s_1_4 92 # ASSIGN : s_1_5 384 # ASSIGN : s_1_6 157 # ASSIGN : s_2_0 210 # ASSIGN : s_2_1 299 # ASSIGN : s_2_2 365 # ASSIGN : s_2_3 122 # ASSIGN : s_2_4 366 # ASSIGN : s_2_5 27 # ASSIGN : s_2_6 2 # ASSIGN : s_3_0 91 # ASSIGN : s_3_1 251 # ASSIGN : s_3_2 392 # ASSIGN : s_3_3 185 # ASSIGN : s_3_4 2 # ASSIGN : s_3_5 210 # ASSIGN : s_3_6 290 # ASSIGN : s_4_0 447 # ASSIGN : s_4_1 205 # ASSIGN : s_4_2 189 # ASSIGN : s_4_3 370 # ASSIGN : s_4_4 342 # ASSIGN : s_4_5 251 # ASSIGN : s_4_6 38 # ASSIGN : s_5_0 13 # ASSIGN : s_5_1 59 # ASSIGN : s_5_2 276 # ASSIGN : s_5_3 215 # ASSIGN : s_5_4 149 # ASSIGN : s_5_5 144 # ASSIGN : s_5_6 356 # ASSIGN : s_6_0 285 # ASSIGN : s_6_1 360 # ASSIGN : s_6_2 146 # ASSIGN : s_6_3 2 # ASSIGN : s_6_4 209 # ASSIGN : s_6_5 182 # ASSIGN : s_6_6 97 SHOW_RESULT 453 END : 453 (0 seconds) [Mon Jun 19 23:17:28 2006] SHOW_RESULT 453 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 451 453 MODIFY_CNF 452 BEGIN : [Mon Jun 19 23:17:28 2006] MODIFY_CNF 452 END : 7581297 bytes (0 seconds) [Mon Jun 19 23:17:28 2006] MODIFY_CNF 452 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 452 BEGIN : [Mon Jun 19 23:17:28 2006] CMD : minisat /tmp/csp2sat14036.cnf /tmp/csp2sat14036.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 270834 782945 | 90278 0 0 nan | 0.000 % | | 100 | 270834 782945 | 99305 100 2706 27.1 | 35.755 % | | 250 | 270834 782945 | 109236 250 8162 32.6 | 35.755 % | | 475 | 270834 782945 | 120160 475 13226 27.8 | 35.755 % | | 812 | 270834 782945 | 132176 812 20886 25.7 | 35.755 % | | 1319 | 270834 782945 | 145393 1319 35504 26.9 | 35.755 % | | 2079 | 270834 782945 | 159932 2079 57419 27.6 | 35.755 % | ============================================================================== restarts : 7 conflicts : 3086 (427 /sec) decisions : 4420 (611 /sec) propagations : 7135067 (986870 /sec) conflict literals : 85465 (16.35 % deleted) Memory used : 17.98 MB CPU time : 7.23 s SATISFIABLE VERIFY_CNF 452 END : (7 seconds) [Mon Jun 19 23:17:35 2006] VERIFY_CNF 452 CPU : 7.28 = 0 + 0 + 7.24 + 0.04 # RESULT : makespan 452 SATISFIABLE SHOW_RESULT 452 BEGIN : [Mon Jun 19 23:17:35 2006] # ASSIGN : makespan 452 # ASSIGN : s_0_0 132 # ASSIGN : s_0_1 219 # ASSIGN : s_0_2 10 # ASSIGN : s_0_3 8 # ASSIGN : s_0_4 309 # ASSIGN : s_0_5 105 # ASSIGN : s_0_6 364 # ASSIGN : s_1_0 14 # ASSIGN : s_1_1 46 # ASSIGN : s_1_2 105 # ASSIGN : s_1_3 357 # ASSIGN : s_1_4 252 # ASSIGN : s_1_5 183 # ASSIGN : s_1_6 317 # ASSIGN : s_2_0 283 # ASSIGN : s_2_1 158 # ASSIGN : s_2_2 9 # ASSIGN : s_2_3 95 # ASSIGN : s_2_4 365 # ASSIGN : s_2_5 19 # ASSIGN : s_2_6 233 # ASSIGN : s_3_0 358 # ASSIGN : s_3_1 7 # ASSIGN : s_3_2 230 # ASSIGN : s_3_3 332 # ASSIGN : s_3_4 63 # ASSIGN : s_3_5 291 # ASSIGN : s_3_6 164 # ASSIGN : s_4_0 8 # ASSIGN : s_4_1 112 # ASSIGN : s_4_2 0 # ASSIGN : s_4_3 18 # ASSIGN : s_4_4 228 # ASSIGN : s_4_5 361 # ASSIGN : s_4_6 258 # ASSIGN : s_5_0 237 # ASSIGN : s_5_1 295 # ASSIGN : s_5_2 372 # ASSIGN : s_5_3 168 # ASSIGN : s_5_4 3 # ASSIGN : s_5_5 286 # ASSIGN : s_5_6 67 # ASSIGN : s_6_0 50 # ASSIGN : s_6_1 359 # ASSIGN : s_6_2 323 # ASSIGN : s_6_3 228 # ASSIGN : s_6_4 152 # ASSIGN : s_6_5 125 # ASSIGN : s_6_6 1 SHOW_RESULT 452 END : 452 (0 seconds) [Mon Jun 19 23:17:35 2006] SHOW_RESULT 452 CPU : 0.0499999999999989 = 0.0499999999999989 + 0 + 0 + 0 # BOUND : makespan 451 452 MODIFY_CNF 451 BEGIN : [Mon Jun 19 23:17:35 2006] MODIFY_CNF 451 END : 7581297 bytes (0 seconds) [Mon Jun 19 23:17:35 2006] MODIFY_CNF 451 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 451 BEGIN : [Mon Jun 19 23:17:35 2006] CMD : minisat /tmp/csp2sat14036.cnf /tmp/csp2sat14036.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 270247 781181 | 90082 0 0 nan | 0.000 % | | 103 | 270247 781181 | 99090 103 3541 34.4 | 35.916 % | | 253 | 270247 781181 | 108999 253 6286 24.8 | 35.916 % | | 479 | 270247 781181 | 119899 479 10502 21.9 | 35.916 % | | 816 | 270247 781181 | 131889 816 17382 21.3 | 35.916 % | | 1322 | 270247 781181 | 145077 1322 30342 23.0 | 35.916 % | | 2083 | 270247 781181 | 159585 2083 49548 23.8 | 35.916 % | | 3222 | 270247 781181 | 175544 3222 74584 23.1 | 35.916 % | | 4931 | 270247 781181 | 193098 4931 120020 24.3 | 35.916 % | ============================================================================== restarts : 9 conflicts : 7268 (407 /sec) decisions : 10302 (576 /sec) propagations : 18416903 (1030605 /sec) conflict literals : 173611 (29.29 % deleted) Memory used : 17.98 MB CPU time : 17.87 s SATISFIABLE VERIFY_CNF 451 END : (18 seconds) [Mon Jun 19 23:17:53 2006] VERIFY_CNF 451 CPU : 17.96 = 0 + 0.01 + 17.89 + 0.06 # RESULT : makespan 451 SATISFIABLE SHOW_RESULT 451 BEGIN : [Mon Jun 19 23:17:53 2006] # ASSIGN : makespan 451 # ASSIGN : s_0_0 16 # ASSIGN : s_0_1 110 # ASSIGN : s_0_2 336 # ASSIGN : s_0_3 108 # ASSIGN : s_0_4 276 # ASSIGN : s_0_5 431 # ASSIGN : s_0_6 188 # ASSIGN : s_1_0 248 # ASSIGN : s_1_1 186 # ASSIGN : s_1_2 100 # ASSIGN : s_1_3 5 # ASSIGN : s_1_4 394 # ASSIGN : s_1_5 285 # ASSIGN : s_1_6 354 # ASSIGN : s_2_0 280 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 450 # ASSIGN : s_2_3 126 # ASSIGN : s_2_4 189 # ASSIGN : s_2_5 355 # ASSIGN : s_2_6 66 # ASSIGN : s_3_0 357 # ASSIGN : s_3_1 61 # ASSIGN : s_3_2 227 # ASSIGN : s_3_3 189 # ASSIGN : s_3_4 100 # ASSIGN : s_3_5 20 # ASSIGN : s_3_6 288 # ASSIGN : s_4_0 188 # ASSIGN : s_4_1 405 # ASSIGN : s_4_2 306 # ASSIGN : s_4_3 314 # ASSIGN : s_4_4 76 # ASSIGN : s_4_5 194 # ASSIGN : s_4_6 7 # ASSIGN : s_5_0 199 # ASSIGN : s_5_1 245 # ASSIGN : s_5_2 11 # ASSIGN : s_5_3 391 # ASSIGN : s_5_4 331 # ASSIGN : s_5_5 189 # ASSIGN : s_5_6 91 # ASSIGN : s_6_0 103 # ASSIGN : s_6_1 309 # ASSIGN : s_6_2 178 # ASSIGN : s_6_3 214 # ASSIGN : s_6_4 0 # ASSIGN : s_6_5 76 # ASSIGN : s_6_6 402 SHOW_RESULT 451 END : 451 (0 seconds) [Mon Jun 19 23:17:53 2006] SHOW_RESULT 451 CPU : 0.0400000000000009 = 0.0400000000000009 + 0 + 0 + 0 # BOUND : makespan 451 451 MAIN END : (45 seconds) [Mon Jun 19 23:17:53 2006] MAIN CPU : 45.25 = 14.72 + 0.06 + 30.09 + 0.38