# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:15:31 2006] READ BEGIN : csp/tai_7x7_2.csp [Mon Jun 19 23:15:31 2006] READ END : csp/tai_7x7_2.csp (0 seconds) [Mon Jun 19 23:15:31 2006] READ CPU : 0.64 = 0.64 + 0 + 0 + 0 # BOUND : makespan 443 619 GENERATE_CNF 619 BEGIN : [Mon Jun 19 23:15:31 2006] GENERATE_CNF 619 END : 31244 variables 372853 clauses 7705153 bytes (15 seconds) [Mon Jun 19 23:15:46 2006] GENERATE_CNF 619 CPU : 14.22 = 14.12 + 0.1 + 0 + 0 MODIFY_CNF 531 BEGIN : [Mon Jun 19 23:15:46 2006] MODIFY_CNF 531 END : 7705158 bytes (0 seconds) [Mon Jun 19 23:15:46 2006] MODIFY_CNF 531 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 531 BEGIN : [Mon Jun 19 23:15:46 2006] CMD : minisat /tmp/csp2sat13971.cnf /tmp/csp2sat13971.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 320173 930704 | 106724 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (19 /sec) decisions : 176 (367 /sec) propagations : 53939 (112373 /sec) conflict literals : 142 (8.39 % deleted) Memory used : 18.12 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 531 END : (0 seconds) [Mon Jun 19 23:15:46 2006] VERIFY_CNF 531 CPU : 0.53 = 0 + 0 + 0.5 + 0.03 # RESULT : makespan 531 SATISFIABLE SHOW_RESULT 531 BEGIN : [Mon Jun 19 23:15:46 2006] # ASSIGN : makespan 531 # ASSIGN : s_0_0 366 # ASSIGN : s_0_1 8 # ASSIGN : s_0_2 268 # ASSIGN : s_0_3 442 # ASSIGN : s_0_4 17 # ASSIGN : s_0_5 21 # ASSIGN : s_0_6 107 # ASSIGN : s_1_0 205 # ASSIGN : s_1_1 447 # ASSIGN : s_1_2 350 # ASSIGN : s_1_3 330 # ASSIGN : s_1_4 44 # ASSIGN : s_1_5 162 # ASSIGN : s_1_6 172 # ASSIGN : s_2_0 6 # ASSIGN : s_2_1 52 # ASSIGN : s_2_2 59 # ASSIGN : s_2_3 268 # ASSIGN : s_2_4 136 # ASSIGN : s_2_5 337 # ASSIGN : s_2_6 211 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 5 # ASSIGN : s_3_2 11 # ASSIGN : s_3_3 57 # ASSIGN : s_3_4 304 # ASSIGN : s_3_5 415 # ASSIGN : s_3_6 270 # ASSIGN : s_4_0 15 # ASSIGN : s_4_1 263 # ASSIGN : s_4_2 496 # ASSIGN : s_4_3 140 # ASSIGN : s_4_4 391 # ASSIGN : s_4_5 426 # ASSIGN : s_4_6 292 # ASSIGN : s_5_0 108 # ASSIGN : s_5_1 280 # ASSIGN : s_5_2 26 # ASSIGN : s_5_3 212 # ASSIGN : s_5_4 424 # ASSIGN : s_5_5 482 # ASSIGN : s_5_6 376 # ASSIGN : s_6_0 302 # ASSIGN : s_6_1 81 # ASSIGN : s_6_2 171 # ASSIGN : s_6_3 370 # ASSIGN : s_6_4 500 # ASSIGN : s_6_5 522 # ASSIGN : s_6_6 431 SHOW_RESULT 531 END : 531 (0 seconds) [Mon Jun 19 23:15:46 2006] SHOW_RESULT 531 CPU : 0.0500000000000011 = 0.0300000000000011 + 0.02 + 0 + 0 # BOUND : makespan 443 531 MODIFY_CNF 487 BEGIN : [Mon Jun 19 23:15:46 2006] MODIFY_CNF 487 END : 7705158 bytes (0 seconds) [Mon Jun 19 23:15:46 2006] MODIFY_CNF 487 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 487 BEGIN : [Mon Jun 19 23:15:46 2006] CMD : minisat /tmp/csp2sat13971.cnf /tmp/csp2sat13971.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 294301 853088 | 98100 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 18 (38 /sec) decisions : 180 (375 /sec) propagations : 64790 (134979 /sec) conflict literals : 255 (9.89 % deleted) Memory used : 18.16 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 487 END : (1 seconds) [Mon Jun 19 23:15:47 2006] VERIFY_CNF 487 CPU : 0.56 = 0 + 0 + 0.5 + 0.06 # RESULT : makespan 487 SATISFIABLE SHOW_RESULT 487 BEGIN : [Mon Jun 19 23:15:47 2006] # ASSIGN : makespan 487 # ASSIGN : s_0_0 314 # ASSIGN : s_0_1 26 # ASSIGN : s_0_2 401 # ASSIGN : s_0_3 225 # ASSIGN : s_0_4 483 # ASSIGN : s_0_5 139 # ASSIGN : s_0_6 35 # ASSIGN : s_1_0 390 # ASSIGN : s_1_1 170 # ASSIGN : s_1_2 293 # ASSIGN : s_1_3 133 # ASSIGN : s_1_4 2 # ASSIGN : s_1_5 254 # ASSIGN : s_1_6 100 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 10 # ASSIGN : s_2_2 17 # ASSIGN : s_2_3 342 # ASSIGN : s_2_4 94 # ASSIGN : s_2_5 264 # ASSIGN : s_2_6 169 # ASSIGN : s_3_0 213 # ASSIGN : s_3_1 401 # ASSIGN : s_3_2 148 # ASSIGN : s_3_3 404 # ASSIGN : s_3_4 260 # ASSIGN : s_3_5 371 # ASSIGN : s_3_6 226 # ASSIGN : s_4_0 20 # ASSIGN : s_4_1 470 # ASSIGN : s_4_2 113 # ASSIGN : s_4_3 153 # ASSIGN : s_4_4 347 # ASSIGN : s_4_5 382 # ASSIGN : s_4_6 248 # ASSIGN : s_5_0 217 # ASSIGN : s_5_1 67 # ASSIGN : s_5_2 163 # ASSIGN : s_5_3 11 # ASSIGN : s_5_4 380 # ASSIGN : s_5_5 438 # ASSIGN : s_5_6 332 # ASSIGN : s_6_0 132 # ASSIGN : s_6_1 297 # ASSIGN : s_6_2 196 # ASSIGN : s_6_3 71 # ASSIGN : s_6_4 456 # ASSIGN : s_6_5 478 # ASSIGN : s_6_6 387 SHOW_RESULT 487 END : 487 (0 seconds) [Mon Jun 19 23:15:47 2006] SHOW_RESULT 487 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 443 487 MODIFY_CNF 465 BEGIN : [Mon Jun 19 23:15:47 2006] MODIFY_CNF 465 END : 7705158 bytes (0 seconds) [Mon Jun 19 23:15:47 2006] MODIFY_CNF 465 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 465 BEGIN : [Mon Jun 19 23:15:47 2006] CMD : minisat /tmp/csp2sat13971.cnf /tmp/csp2sat13971.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 281365 814280 | 93788 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 40 (75 /sec) decisions : 191 (360 /sec) propagations : 109361 (206342 /sec) conflict literals : 1129 (5.76 % deleted) Memory used : 18.16 MB CPU time : 0.53 s SATISFIABLE VERIFY_CNF 465 END : (1 seconds) [Mon Jun 19 23:15:48 2006] VERIFY_CNF 465 CPU : 0.6 = 0 + 0 + 0.55 + 0.05 # RESULT : makespan 465 SATISFIABLE SHOW_RESULT 465 BEGIN : [Mon Jun 19 23:15:48 2006] # ASSIGN : makespan 465 # ASSIGN : s_0_0 288 # ASSIGN : s_0_1 367 # ASSIGN : s_0_2 195 # ASSIGN : s_0_3 376 # ASSIGN : s_0_4 191 # ASSIGN : s_0_5 105 # ASSIGN : s_0_6 40 # ASSIGN : s_1_0 368 # ASSIGN : s_1_1 139 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 348 # ASSIGN : s_1_4 233 # ASSIGN : s_1_5 223 # ASSIGN : s_1_6 106 # ASSIGN : s_2_0 202 # ASSIGN : s_2_1 253 # ASSIGN : s_2_2 338 # ASSIGN : s_2_3 75 # ASSIGN : s_2_4 0 # ASSIGN : s_2_5 260 # ASSIGN : s_2_6 145 # ASSIGN : s_3_0 364 # ASSIGN : s_3_1 6 # ASSIGN : s_3_2 415 # ASSIGN : s_3_3 265 # ASSIGN : s_3_4 104 # ASSIGN : s_3_5 349 # ASSIGN : s_3_6 204 # ASSIGN : s_4_0 12 # ASSIGN : s_4_1 120 # ASSIGN : s_4_2 430 # ASSIGN : s_4_3 137 # ASSIGN : s_4_4 325 # ASSIGN : s_4_5 360 # ASSIGN : s_4_6 226 # ASSIGN : s_5_0 105 # ASSIGN : s_5_1 9 # ASSIGN : s_5_2 277 # ASSIGN : s_5_3 209 # ASSIGN : s_5_4 358 # ASSIGN : s_5_5 416 # ASSIGN : s_5_6 310 # ASSIGN : s_6_0 211 # ASSIGN : s_6_1 275 # ASSIGN : s_6_2 98 # ASSIGN : s_6_3 14 # ASSIGN : s_6_4 434 # ASSIGN : s_6_5 456 # ASSIGN : s_6_6 365 SHOW_RESULT 465 END : 465 (0 seconds) [Mon Jun 19 23:15:48 2006] SHOW_RESULT 465 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 443 465 MODIFY_CNF 454 BEGIN : [Mon Jun 19 23:15:48 2006] MODIFY_CNF 454 END : 7705158 bytes (0 seconds) [Mon Jun 19 23:15:48 2006] MODIFY_CNF 454 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 454 BEGIN : [Mon Jun 19 23:15:48 2006] CMD : minisat /tmp/csp2sat13971.cnf /tmp/csp2sat13971.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 274897 794876 | 91632 0 0 nan | 0.000 % | | 100 | 274897 794876 | 100795 100 3149 31.5 | 35.408 % | ============================================================================== restarts : 2 conflicts : 107 (147 /sec) decisions : 298 (408 /sec) propagations : 291365 (399130 /sec) conflict literals : 3207 (17.43 % deleted) Memory used : 18.18 MB CPU time : 0.73 s SATISFIABLE VERIFY_CNF 454 END : (1 seconds) [Mon Jun 19 23:15:49 2006] VERIFY_CNF 454 CPU : 0.8 = 0 + 0 + 0.74 + 0.06 # RESULT : makespan 454 SATISFIABLE SHOW_RESULT 454 BEGIN : [Mon Jun 19 23:15:49 2006] # ASSIGN : makespan 454 # ASSIGN : s_0_0 122 # ASSIGN : s_0_1 198 # ASSIGN : s_0_2 40 # ASSIGN : s_0_3 293 # ASSIGN : s_0_4 13 # ASSIGN : s_0_5 207 # ASSIGN : s_0_6 389 # ASSIGN : s_1_0 21 # ASSIGN : s_1_1 360 # ASSIGN : s_1_2 131 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 268 # ASSIGN : s_1_5 444 # ASSIGN : s_1_6 235 # ASSIGN : s_2_0 8 # ASSIGN : s_2_1 1 # ASSIGN : s_2_2 263 # ASSIGN : s_2_3 92 # ASSIGN : s_2_4 17 # ASSIGN : s_2_5 366 # ASSIGN : s_2_6 178 # ASSIGN : s_3_0 118 # ASSIGN : s_3_1 207 # ASSIGN : s_3_2 340 # ASSIGN : s_3_3 210 # ASSIGN : s_3_4 367 # ASSIGN : s_3_5 355 # ASSIGN : s_3_6 156 # ASSIGN : s_4_0 264 # ASSIGN : s_4_1 214 # ASSIGN : s_4_2 5 # ASSIGN : s_4_3 382 # ASSIGN : s_4_4 231 # ASSIGN : s_4_5 151 # ASSIGN : s_4_6 67 # ASSIGN : s_5_0 357 # ASSIGN : s_5_1 261 # ASSIGN : s_5_2 228 # ASSIGN : s_5_3 154 # ASSIGN : s_5_4 96 # ASSIGN : s_5_5 56 # ASSIGN : s_5_6 8 # ASSIGN : s_6_0 200 # ASSIGN : s_6_1 88 # ASSIGN : s_6_2 357 # ASSIGN : s_6_3 27 # ASSIGN : s_6_4 178 # ASSIGN : s_6_5 346 # ASSIGN : s_6_6 277 SHOW_RESULT 454 END : 454 (0 seconds) [Mon Jun 19 23:15:49 2006] SHOW_RESULT 454 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 443 454 MODIFY_CNF 448 BEGIN : [Mon Jun 19 23:15:49 2006] MODIFY_CNF 448 END : 7705157 bytes (0 seconds) [Mon Jun 19 23:15:49 2006] MODIFY_CNF 448 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 448 BEGIN : [Mon Jun 19 23:15:49 2006] CMD : minisat /tmp/csp2sat13971.cnf /tmp/csp2sat13971.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 271369 784292 | 90456 0 0 nan | 0.000 % | | 101 | 271369 784292 | 99501 101 2109 20.9 | 36.369 % | ============================================================================== restarts : 2 conflicts : 154 (179 /sec) decisions : 334 (388 /sec) propagations : 399058 (464021 /sec) conflict literals : 3192 (25.63 % deleted) Memory used : 18.18 MB CPU time : 0.86 s SATISFIABLE VERIFY_CNF 448 END : (1 seconds) [Mon Jun 19 23:15:50 2006] VERIFY_CNF 448 CPU : 0.89 = 0 + 0 + 0.87 + 0.02 # RESULT : makespan 448 SATISFIABLE SHOW_RESULT 448 BEGIN : [Mon Jun 19 23:15:50 2006] # ASSIGN : makespan 448 # ASSIGN : s_0_0 113 # ASSIGN : s_0_1 429 # ASSIGN : s_0_2 254 # ASSIGN : s_0_3 339 # ASSIGN : s_0_4 444 # ASSIGN : s_0_5 27 # ASSIGN : s_0_6 189 # ASSIGN : s_1_0 190 # ASSIGN : s_1_1 311 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 428 # ASSIGN : s_1_4 98 # ASSIGN : s_1_5 301 # ASSIGN : s_1_6 395 # ASSIGN : s_2_0 4 # ASSIGN : s_2_1 441 # ASSIGN : s_2_2 177 # ASSIGN : s_2_3 88 # ASSIGN : s_2_4 13 # ASSIGN : s_2_5 363 # ASSIGN : s_2_6 254 # ASSIGN : s_3_0 109 # ASSIGN : s_3_1 438 # ASSIGN : s_3_2 336 # ASSIGN : s_3_3 5 # ASSIGN : s_3_4 351 # ASSIGN : s_3_5 325 # ASSIGN : s_3_6 167 # ASSIGN : s_4_0 16 # ASSIGN : s_4_1 412 # ASSIGN : s_4_2 109 # ASSIGN : s_4_3 150 # ASSIGN : s_4_4 278 # ASSIGN : s_4_5 222 # ASSIGN : s_4_6 311 # ASSIGN : s_5_0 351 # ASSIGN : s_5_1 0 # ASSIGN : s_5_2 144 # ASSIGN : s_5_3 283 # ASSIGN : s_5_4 220 # ASSIGN : s_5_5 180 # ASSIGN : s_5_6 96 # ASSIGN : s_6_0 287 # ASSIGN : s_6_1 108 # ASSIGN : s_6_2 351 # ASSIGN : s_6_3 222 # ASSIGN : s_6_4 198 # ASSIGN : s_6_5 18 # ASSIGN : s_6_6 27 SHOW_RESULT 448 END : 448 (0 seconds) [Mon Jun 19 23:15:50 2006] SHOW_RESULT 448 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 443 448 MODIFY_CNF 445 BEGIN : [Mon Jun 19 23:15:50 2006] MODIFY_CNF 445 END : 7705157 bytes (0 seconds) [Mon Jun 19 23:15:50 2006] MODIFY_CNF 445 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 445 BEGIN : [Mon Jun 19 23:15:50 2006] CMD : minisat /tmp/csp2sat13971.cnf /tmp/csp2sat13971.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 269605 779000 | 89868 0 0 nan | 0.000 % | | 102 | 269605 779000 | 98854 102 2259 22.1 | 36.849 % | | 252 | 269605 779000 | 108740 252 6466 25.7 | 36.849 % | ============================================================================== restarts : 3 conflicts : 288 (274 /sec) decisions : 538 (512 /sec) propagations : 652963 (621870 /sec) conflict literals : 7029 (16.82 % deleted) Memory used : 18.18 MB CPU time : 1.05 s SATISFIABLE VERIFY_CNF 445 END : (1 seconds) [Mon Jun 19 23:15:51 2006] VERIFY_CNF 445 CPU : 1.16 = 0.00999999999999979 + 0.01 + 1.07 + 0.07 # RESULT : makespan 445 SATISFIABLE SHOW_RESULT 445 BEGIN : [Mon Jun 19 23:15:51 2006] # ASSIGN : makespan 445 # ASSIGN : s_0_0 7 # ASSIGN : s_0_1 265 # ASSIGN : s_0_2 363 # ASSIGN : s_0_3 274 # ASSIGN : s_0_4 259 # ASSIGN : s_0_5 173 # ASSIGN : s_0_6 97 # ASSIGN : s_1_0 189 # ASSIGN : s_1_1 8 # ASSIGN : s_1_2 92 # ASSIGN : s_1_3 425 # ASSIGN : s_1_4 333 # ASSIGN : s_1_5 286 # ASSIGN : s_1_6 300 # ASSIGN : s_2_0 83 # ASSIGN : s_2_1 92 # ASSIGN : s_2_2 286 # ASSIGN : s_2_3 212 # ASSIGN : s_2_4 119 # ASSIGN : s_2_5 5 # ASSIGN : s_2_6 388 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 7 # ASSIGN : s_3_3 129 # ASSIGN : s_3_4 32 # ASSIGN : s_3_5 394 # ASSIGN : s_3_6 366 # ASSIGN : s_4_0 352 # ASSIGN : s_4_1 246 # ASSIGN : s_4_2 22 # ASSIGN : s_4_3 57 # ASSIGN : s_4_4 263 # ASSIGN : s_4_5 296 # ASSIGN : s_4_6 162 # ASSIGN : s_5_0 92 # ASSIGN : s_5_1 309 # ASSIGN : s_5_2 59 # ASSIGN : s_5_3 1 # ASSIGN : s_5_4 194 # ASSIGN : s_5_5 405 # ASSIGN : s_5_6 252 # ASSIGN : s_6_0 288 # ASSIGN : s_6_1 99 # ASSIGN : s_6_2 189 # ASSIGN : s_6_3 364 # ASSIGN : s_6_4 6 # ASSIGN : s_6_5 355 # ASSIGN : s_6_6 28 SHOW_RESULT 445 END : 445 (0 seconds) [Mon Jun 19 23:15:51 2006] SHOW_RESULT 445 CPU : 0.0399999999999993 = 0.0299999999999994 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 443 445 MODIFY_CNF 444 BEGIN : [Mon Jun 19 23:15:51 2006] MODIFY_CNF 444 END : 7705157 bytes (0 seconds) [Mon Jun 19 23:15:51 2006] MODIFY_CNF 444 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 444 BEGIN : [Mon Jun 19 23:15:51 2006] CMD : minisat /tmp/csp2sat13971.cnf /tmp/csp2sat13971.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 269017 777236 | 89672 0 0 nan | 0.000 % | | 100 | 269017 777236 | 98639 100 2586 25.9 | 37.009 % | | 250 | 269017 777236 | 108503 250 5460 21.8 | 37.009 % | | 476 | 269017 777236 | 119353 476 8867 18.6 | 37.009 % | | 813 | 269017 777236 | 131288 813 15419 19.0 | 37.009 % | ============================================================================== restarts : 5 conflicts : 826 (374 /sec) decisions : 1333 (603 /sec) propagations : 1938268 (877044 /sec) conflict literals : 15549 (25.23 % deleted) Memory used : 18.18 MB CPU time : 2.21 s SATISFIABLE VERIFY_CNF 444 END : (2 seconds) [Mon Jun 19 23:15:53 2006] VERIFY_CNF 444 CPU : 2.27 = 0 + 0 + 2.23 + 0.04 # RESULT : makespan 444 SATISFIABLE SHOW_RESULT 444 BEGIN : [Mon Jun 19 23:15:53 2006] # ASSIGN : makespan 444 # ASSIGN : s_0_0 271 # ASSIGN : s_0_1 5 # ASSIGN : s_0_2 188 # ASSIGN : s_0_3 83 # ASSIGN : s_0_4 14 # ASSIGN : s_0_5 358 # ASSIGN : s_0_6 18 # ASSIGN : s_1_0 164 # ASSIGN : s_1_1 263 # ASSIGN : s_1_2 347 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 39 # ASSIGN : s_1_5 26 # ASSIGN : s_1_6 131 # ASSIGN : s_2_0 261 # ASSIGN : s_2_1 362 # ASSIGN : s_2_2 270 # ASSIGN : s_2_3 21 # ASSIGN : s_2_4 369 # ASSIGN : s_2_5 95 # ASSIGN : s_2_6 173 # ASSIGN : s_3_0 67 # ASSIGN : s_3_1 441 # ASSIGN : s_3_2 173 # ASSIGN : s_3_3 300 # ASSIGN : s_3_4 202 # ASSIGN : s_3_5 289 # ASSIGN : s_3_6 109 # ASSIGN : s_4_0 71 # ASSIGN : s_4_1 19 # ASSIGN : s_4_2 36 # ASSIGN : s_4_3 228 # ASSIGN : s_4_4 169 # ASSIGN : s_4_5 302 # ASSIGN : s_4_6 360 # ASSIGN : s_5_0 347 # ASSIGN : s_5_1 76 # ASSIGN : s_5_2 3 # ASSIGN : s_5_3 172 # ASSIGN : s_5_4 289 # ASSIGN : s_5_5 36 # ASSIGN : s_5_6 230 # ASSIGN : s_6_0 3 # ASSIGN : s_6_1 173 # ASSIGN : s_6_2 76 # ASSIGN : s_6_3 383 # ASSIGN : s_6_4 347 # ASSIGN : s_6_5 269 # ASSIGN : s_6_6 278 SHOW_RESULT 444 END : 444 (0 seconds) [Mon Jun 19 23:15:53 2006] SHOW_RESULT 444 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 443 444 MODIFY_CNF 443 BEGIN : [Mon Jun 19 23:15:53 2006] MODIFY_CNF 443 END : 7705157 bytes (0 seconds) [Mon Jun 19 23:15:53 2006] MODIFY_CNF 443 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 443 BEGIN : [Mon Jun 19 23:15:53 2006] CMD : minisat /tmp/csp2sat13971.cnf /tmp/csp2sat13971.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 268430 775472 | 89476 0 0 nan | 0.000 % | | 101 | 268430 775472 | 98423 101 1795 17.8 | 37.169 % | | 252 | 268430 775472 | 108265 252 4785 19.0 | 37.169 % | | 477 | 268430 775472 | 119092 477 9125 19.1 | 37.169 % | ============================================================================== restarts : 4 conflicts : 773 (345 /sec) decisions : 1377 (615 /sec) propagations : 1930573 (861863 /sec) conflict literals : 14377 (24.29 % deleted) Memory used : 18.18 MB CPU time : 2.24 s SATISFIABLE VERIFY_CNF 443 END : (2 seconds) [Mon Jun 19 23:15:55 2006] VERIFY_CNF 443 CPU : 2.35 = 0 + 0 + 2.26 + 0.09 # RESULT : makespan 443 SATISFIABLE SHOW_RESULT 443 BEGIN : [Mon Jun 19 23:15:55 2006] # ASSIGN : makespan 443 # ASSIGN : s_0_0 269 # ASSIGN : s_0_1 345 # ASSIGN : s_0_2 2 # ASSIGN : s_0_3 354 # ASSIGN : s_0_4 200 # ASSIGN : s_0_5 84 # ASSIGN : s_0_6 204 # ASSIGN : s_1_0 11 # ASSIGN : s_1_1 359 # ASSIGN : s_1_2 166 # ASSIGN : s_1_3 144 # ASSIGN : s_1_4 264 # ASSIGN : s_1_5 1 # ASSIGN : s_1_6 111 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 253 # ASSIGN : s_2_2 87 # ASSIGN : s_2_3 164 # ASSIGN : s_2_4 12 # ASSIGN : s_2_5 260 # ASSIGN : s_2_6 338 # ASSIGN : s_3_0 346 # ASSIGN : s_3_1 342 # ASSIGN : s_3_2 296 # ASSIGN : s_3_3 61 # ASSIGN : s_3_4 356 # ASSIGN : s_3_5 249 # ASSIGN : s_3_6 182 # ASSIGN : s_4_0 350 # ASSIGN : s_4_1 98 # ASSIGN : s_4_2 311 # ASSIGN : s_4_3 226 # ASSIGN : s_4_4 137 # ASSIGN : s_4_5 170 # ASSIGN : s_4_6 14 # ASSIGN : s_5_0 108 # ASSIGN : s_5_1 2 # ASSIGN : s_5_2 263 # ASSIGN : s_5_3 298 # ASSIGN : s_5_4 205 # ASSIGN : s_5_5 355 # ASSIGN : s_5_6 395 # ASSIGN : s_6_0 205 # ASSIGN : s_6_1 115 # ASSIGN : s_6_2 346 # ASSIGN : s_6_3 0 # ASSIGN : s_6_4 93 # ASSIGN : s_6_5 75 # ASSIGN : s_6_6 269 SHOW_RESULT 443 END : 443 (0 seconds) [Mon Jun 19 23:15:55 2006] SHOW_RESULT 443 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 443 443 MAIN END : (24 seconds) [Mon Jun 19 23:15:55 2006] MAIN CPU : 24.38 = 15.1 + 0.14 + 8.72 + 0.42