Name | normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen2.opb |
MD5SUM | 30256c883dd8af773c334a2b26410bd9 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 9400 |
Biggest coefficient in the objective function | 2494038016 |
Number of bits for the biggest coefficient in the objective function | 32 |
Sum of the numbers in the objective function | 391862963250 |
Number of bits of the sum of numbers in the objective function | 39 |
Biggest number in a constraint | 2494038016 |
Number of bits of the biggest number in a constraint | 32 |
Biggest sum of numbers in a constraint | 391862963250 |
Number of bits of the biggest sum of numbers | 39 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.092985 |
Number of variables | 10680 |
Total number of constraints | 444 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 444 |
Minimum length of a constraint | 40 |
Maximum length of a constraint | 1700 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc28 THE 2005-04-21 20:02:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=15690 boxname=wulflinc28 idbench=1207 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 30256c883dd8af773c334a2b26410bd9 /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-degen2.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-degen2.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-degen2.opb IDLAUNCH: 15690 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 434032 kB Buffers: 34780 kB Cached: 538356 kB SwapCached: 104 kB Active: 209112 kB Inactive: 366424 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 433780 kB SwapTotal: 2097640 kB SwapFree: 2097068 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6056 kB Slab: 19448 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 20:22:05 (client local time) WITH STATUS 0 IN 1200.4 SECONDS stats: 15690 7 1200.4 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 665 PB-constraints to clauses... c -- Unit propagations: ppp c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################# c -- Clauses(.)/Splits(s): sss c ---[ 667]---> BDD-cost:59412 c ---[ 666]---> BDD-cost:52284 c ---[ 665]---> BDD-cost:32923 c ---[ 663]---> BDD-cost: 1280 c ---[ 661]---> BDD-cost: 1280 c ---[ 659]---> BDD-cost: 2580 c ---[ 657]---> BDD-cost: 2579 c ---[ 655]---> BDD-cost: 302 c ---[ 653]---> BDD-cost: 302 c ---[ 651]---> BDD-cost: 866 c ---[ 649]---> BDD-cost: 866 c ---[ 647]---> BDD-cost: 9173 c ---[ 645]---> BDD-cost:10298 c ---[ 643]---> BDD-cost: 866 c ---[ 641]---> BDD-cost: 866 c ---[ 639]---> BDD-cost: 3943 c ---[ 637]---> BDD-cost: 3943 c ---[ 635]---> BDD-cost: 564 c ---[ 633]---> BDD-cost: 564 c ---[ 631]---> BDD-cost: 3943 c ---[ 629]---> BDD-cost: 4330 c ---[ 627]---> BDD-cost: 22 c ---[ 625]---> BDD-cost: 1746 c ---[ 623]---> BDD-cost: 1746 c ---[ 621]---> BDD-cost:15125 c ---[ 619]---> BDD-cost:13684 c ---[ 617]---> BDD-cost: 302 c ---[ 615]---> BDD-cost: 302 c ---[ 613]---> BDD-cost: 302 c ---[ 611]---> BDD-cost: 301 c ---[ 609]---> BDD-cost:25312 c ---[ 607]---> BDD-cost:26347 c ---[ 605]---> BDD-cost: 302 c ---[ 603]---> BDD-cost: 302 c ---[ 601]---> BDD-cost: 1280 c ---[ 599]---> BDD-cost: 1280 c ---[ 597]---> BDD-cost: 302 c ---[ 595]---> BDD-cost: 302 c ---[ 593]---> BDD-cost: 128 c ---[ 591]---> BDD-cost: 128 c ---[ 589]---> BDD-cost: 302 c ---[ 587]---> BDD-cost: 302 c ---[ 585]---> BDD-cost: 2316 c ---[ 583]---> BDD-cost: 2316 c ---[ 581]---> BDD-cost: 8706 c ---[ 579]---> BDD-cost: 9308 c ---[ 577]---> BDD-cost: 64 c ---[ 576]---> BDD-cost: 131 c ---[ 575]---> BDD-cost: 130 c ---[ 574]---> BDD-cost: 130 c ---[ 573]---> BDD-cost: 316 c ---[ 572]---> BDD-cost: 315 c ---[ 571]---> BDD-cost: 315 c ---[ 570]---> BDD-cost: 558 c ---[ 569]---> BDD-cost: 557 c ---[ 568]---> BDD-cost: 557 c ---[ 567]---> BDD-cost: 26 c ---[ 566]---> BDD-cost: 128 c ---[ 565]---> BDD-cost: 67 c ---[ 564]---> BDD-cost: 67 c ---[ 563]---> BDD-cost: 565 c ---[ 562]---> BDD-cost: 434 c ---[ 561]---> BDD-cost: 205 c ---[ 560]---> BDD-cost: 895 c ---[ 559]---> BDD-cost: 708 c ---[ 558]---> BDD-cost: 68 c ---[ 557]---> BDD-cost: 67 c ---[ 556]---> BDD-cost: 67 c ---[ 555]---> BDD-cost: 68 c ---[ 554]---> BDD-cost: 67 c ---[ 553]---> BDD-cost: 67 c ---[ 552]---> BDD-cost: 200 c ---[ 551]---> BDD-cost: 199 c ---[ 550]---> BDD-cost: 205 c ---[ 549]---> BDD-cost: 422 c ---[ 548]---> BDD-cost: 421 c ---[ 547]---> BDD-cost: 425 c ---[ 546]---> BDD-cost: 435 c ---[ 545]---> BDD-cost: 424 c ---[ 544]---> BDD-cost: 434 c ---[ 543]---> BDD-cost: 1110 c ---[ 542]---> BDD-cost: 1100 c ---[ 541]---> BDD-cost: 1109 c ---[ 540]---> BDD-cost: 1821 c ---[ 539]---> BDD-cost: 2067 c ---[ 538]---> BDD-cost: 2080 c ---[ 537]---> BDD-cost: 2392 c ---[ 536]---> BDD-cost: 2690 c ---[ 535]---> BDD-cost: 2705 c ---[ 534]---> BDD-cost: 4147 c ---[ 533]---> BDD-cost: 4940 c ---[ 532]---> BDD-cost: 4965 c ---[ 531]---> BDD-cost: 5443 c ---[ 530]---> BDD-cost: 6317 c ---[ 529]---> BDD-cost: 6342 c ---[ 528]---> BDD-cost: 6426 c ---[ 527]---> BDD-cost: 7372 c ---[ 526]---> BDD-cost: 7399 c ---[ 525]---> BDD-cost: 7354 c ---[ 524]---> BDD-cost: 8400 c ---[ 523]---> BDD-cost: 8443 c ---[ 522]---> BDD-cost: 68 c ---[ 521]---> BDD-cost: 67 c ---[ 520]---> BDD-cost: 67 c ---[ 519]---> BDD-cost: 206 c ---[ 518]---> BDD-cost: 205 c ---[ 517]---> BDD-cost: 205 c ---[ 516]---> BDD-cost: 435 c ---[ 515]---> BDD-cost: 434 c ---[ 514]---> BDD-cost: 434 c ---[ 513]---> BDD-cost: 318 c ---[ 512]---> BDD-cost: 317 c ---[ 511]---> BDD-cost: 581 c ---[ 510]---> BDD-cost: 580 c ---[ 509]---> BDD-cost: 67 c ---[ 508]---> BDD-cost: 205 c ---[ 507]---> BDD-cost: 1140 c ---[ 506]---> BDD-cost: 1139 c ---[ 505]---> BDD-cost: 310 c ---[ 504]---> BDD-cost: 2123 c ---[ 503]---> BDD-cost: 2122 c ---[ 502]---> BDD-cost: 564 c ---[ 501]---> BDD-cost: 2725 c ---[ 500]---> BDD-cost: 2724 c ---[ 499]---> BDD-cost: 200 c ---[ 498]---> BDD-cost: 199 c ---[ 497]---> BDD-cost: 68 c ---[ 496]---> BDD-cost: 67 c ---[ 495]---> BDD-cost: 711 c ---[ 494]---> BDD-cost: 710 c ---[ 493]---> BDD-cost: 1299 c ---[ 492]---> BDD-cost: 1522 c ---[ 491]---> BDD-cost: 119 c ---[ 490]---> BDD-cost: 68 c ---[ 489]---> BDD-cost: 67 c ---[ 488]---> BDD-cost: 67 c ---[ 487]---> BDD-cost: 204 c ---[ 486]---> BDD-cost: 203 c ---[ 485]---> BDD-cost: 205 c ---[ 484]---> BDD-cost: 429 c ---[ 483]---> BDD-cost: 428 c ---[ 482]---> BDD-cost: 434 c ---[ 481]---> BDD-cost: 696 c ---[ 480]---> BDD-cost: 695 c ---[ 479]---> BDD-cost: 701 c ---[ 478]---> BDD-cost: 1072 c ---[ 477]---> BDD-cost: 1071 c ---[ 476]---> BDD-cost: 1073 c ---[ 475]---> BDD-cost: 120 c ---[ 474]---> BDD-cost: 127 c ---[ 473]---> BDD-cost: 517 c ---[ 472]---> BDD-cost: 537 c ---[ 471]---> BDD-cost: 1014 c ---[ 470]---> BDD-cost: 67 c ---[ 469]---> BDD-cost: 203 c ---[ 468]---> BDD-cost: 2338 c ---[ 467]---> BDD-cost: 2034 c ---[ 466]---> BDD-cost: 2879 c ---[ 465]---> BDD-cost: 2599 c ---[ 464]---> BDD-cost: 434 c ---[ 463]---> BDD-cost: 3659 c ---[ 462]---> BDD-cost: 4092 c ---[ 461]---> BDD-cost: 5239 c ---[ 460]---> BDD-cost: 4762 c ---[ 459]---> BDD-cost: 875 c ---[ 458]---> BDD-cost: 8118 c ---[ 457]---> BDD-cost: 9314 c ---[ 456]---> BDD-cost: 8713 c ---[ 455]---> BDD-cost: 66 c ---[ 454]---> BDD-cost: 65 c ---[ 453]---> BDD-cost: 67 c ---[ 452]---> BDD-cost: 204 c ---[ 451]---> BDD-cost: 203 c ---[ 450]---> BDD-cost: 203 c ---[ 449]---> BDD-cost: 25 c ---[ 448]---> BDD-cost: 130 c ---[ 447]---> BDD-cost: 68 c ---[ 446]---> BDD-cost: 127 c ---[ 445]---> BDD-cost: 313 c ---[ 442]---> BDD-cost: 190 c ---[ 441]---> BDD-cost: 202 c ---[ 440]---> BDD-cost: 127 c ---[ 439]---> BDD-cost: 1355 c ---[ 438]---> BDD-cost: 939 c ---[ 437]---> BDD-cost: 1356 c ---[ 436]---> BDD-cost: 1831 c ---[ 435]---> BDD-cost: 1355 c ---[ 434]---> BDD-cost: 3080 c ---[ 433]---> BDD-cost: 3464 c ---[ 432]---> BDD-cost: 2744 c ---[ 431]---> BDD-cost: 3784 c ---[ 430]---> BDD-cost: 4169 c ---[ 429]---> BDD-cost: 4912 c ---[ 428]---> BDD-cost: 5824 c ---[ 427]---> BDD-cost: 6406 c ---[ 426]---> BDD-cost: 4995 c ---[ 425]---> BDD-cost: 5269 c ---[ 424]---> BDD-cost: 7933 c ---[ 423]---> BDD-cost: 8563 c ---[ 422]---> BDD-cost: 7008 c ---[ 421]---> BDD-cost:11719 c ---[ 420]---> BDD-cost:12366 c ---[ 419]---> BDD-cost: 9726 c ---[ 418]---> BDD-cost:15879 c ---[ 417]---> BDD-cost:16633 c ---[ 416]---> BDD-cost:13571 c ---[ 415]---> BDD-cost:18390 c ---[ 414]---> BDD-cost:19057 c ---[ 413]---> BDD-cost:15905 c ---[ 412]---> BDD-cost:20892 c ---[ 411]---> BDD-cost:21722 c ---[ 410]---> BDD-cost:18260 c ---[ 409]---> BDD-cost: 27 c ---[ 408]---> BDD-cost: 131 c ---[ 407]---> BDD-cost: 67 c ---[ 406]---> BDD-cost: 67 c ---[ 405]---> BDD-cost: 68 c ---[ 404]---> BDD-cost: 67 c ---[ 403]---> BDD-cost: 206 c ---[ 402]---> BDD-cost: 205 c ---[ 401]---> BDD-cost: 435 c ---[ 400]---> BDD-cost: 434 c ---[ 399]---> BDD-cost: 68 c ---[ 398]---> BDD-cost: 67 c ---[ 397]---> BDD-cost: 206 c ---[ 396]---> BDD-cost: 205 c ---[ 395]---> BDD-cost: 67 c ---[ 394]---> BDD-cost: 68 c ---[ 393]---> BDD-cost: 67 c ---[ 392]---> BDD-cost: 67 c ---[ 391]---> BDD-cost: 66 c ---[ 390]---> BDD-cost: 65 c ---[ 389]---> BDD-cost: 67 c ---[ 388]---> BDD-cost: 0 c ---[ 387]---> BDD-cost: 202 c ---[ 386]---> BDD-cost: 201 c ---[ 385]---> BDD-cost: 203 c ---[ 384]---> BDD-cost: 68 c ---[ 383]---> BDD-cost: 67 c ---[ 382]---> BDD-cost: 67 c ---[ 381]---> BDD-cost: 204 c ---[ 380]---> BDD-cost: 203 c ---[ 379]---> BDD-cost: 551 c ---[ 378]---> BDD-cost: 550 c ---[ 377]---> BDD-cost: 299 c ---[ 376]---> BDD-cost: 67 c ---[ 374]---> BDD-cost: 131 c ---[ 373]---> BDD-cost: 205 c ---[ 372]---> BDD-cost: 130 c ---[ 371]---> BDD-cost: 1090 c ---[ 370]---> BDD-cost: 1298 c ---[ 369]---> BDD-cost: 1825 c ---[ 368]---> BDD-cost: 2097 c ---[ 367]---> BDD-cost: 2373 c ---[ 366]---> BDD-cost: 2631 c ---[ 365]---> BDD-cost: 432 c ---[ 364]---> BDD-cost: 2954 c ---[ 363]---> BDD-cost: 3300 c ---[ 362]---> BDD-cost: 5984 c ---[ 361]---> BDD-cost: 6164 c ---[ 360]---> BDD-cost: 6805 c ---[ 359]---> BDD-cost: 6932 c ---[ 358]---> BDD-cost: 65 c ---[ 357]---> BDD-cost: 67 c ---[ 355]---> BDD-cost: 35 c ---[ 353]---> BDD-cost: 35 c ---[ 351]---> BDD-cost: 35 c ---[ 349]---> BDD-cost: 35 c ---[ 347]---> BDD-cost: 35 c ---[ 345]---> BDD-cost: 35 c ---[ 343]---> BDD-cost: 35 c ---[ 341]---> BDD-cost: 35 c ---[ 339]---> BDD-cost: 35 c ---[ 337]---> BDD-cost: 35 c ---[ 335]---> BDD-cost: 35 c ---[ 333]---> BDD-cost: 35 c ---[ 331]---> BDD-cost: 35 c ---[ 329]---> BDD-cost: 35 c ---[ 327]---> BDD-cost: 35 c ---[ 325]---> BDD-cost: 35 c ---[ 323]---> BDD-cost: 35 c ---[ 321]---> BDD-cost: 35 c ---[ 319]---> BDD-cost: 76 c ---[ 317]---> BDD-cost: 76 c ---[ 315]---> BDD-cost: 35 c ---[ 313]---> BDD-cost: 35 c ---[ 311]---> BDD-cost: 35 c ---[ 309]---> BDD-cost: 35 c ---[ 307]---> BDD-cost: 35 c ---[ 305]---> BDD-cost: 35 c ---[ 303]---> BDD-cost: 35 c ---[ 301]---> BDD-cost: 35 c ---[ 299]---> BDD-cost: 35 c ---[ 297]---> BDD-cost: 35 c ---[ 295]---> BDD-cost: 35 c ---[ 293]---> BDD-cost: 35 c ---[ 291]---> BDD-cost: 76 c ---[ 289]---> BDD-cost: 35 c ---[ 287]---> BDD-cost: 35 c ---[ 285]---> BDD-cost: 35 c ---[ 283]---> BDD-cost: 35 c ---[ 281]---> BDD-cost: 35 c ---[ 279]---> BDD-cost: 35 c ---[ 277]---> BDD-cost: 35 c ---[ 275]---> BDD-cost: 35 c ---[ 273]---> BDD-cost: 35 c ---[ 271]---> BDD-cost: 35 c ---[ 269]---> BDD-cost: 35 c ---[ 267]---> BDD-cost: 35 c ---[ 265]---> BDD-cost: 35 c ---[ 263]---> BDD-cost: 35 c ---[ 261]---> BDD-cost: 35 c ---[ 259]---> BDD-cost: 35 c ---[ 257]---> BDD-cost: 35 c ---[ 255]---> BDD-cost: 35 c ---[ 253]---> BDD-cost: 35 c ---[ 251]---> BDD-cost: 35 c ---[ 249]---> BDD-cost: 35 c ---[ 247]---> BDD-cost: 35 c ---[ 245]---> BDD-cost: 35 c ---[ 243]---> BDD-cost: 35 c ---[ 241]---> BDD-cost: 35 c ---[ 239]---> BDD-cost: 35 c ---[ 237]---> BDD-cost: 76 c ---[ 235]---> BDD-cost: 76 c ---[ 233]---> BDD-cost: 76 c ---[ 231]---> BDD-cost: 76 c ---[ 229]---> BDD-cost: 76 c ---[ 227]---> BDD-cost: 76 c ---[ 225]---> BDD-cost: 76 c ---[ 223]---> BDD-cost: 76 c ---[ 221]---> BDD-cost: 76 c ---[ 219]---> BDD-cost: 76 c ---[ 217]---> BDD-cost: 76 c ---[ 215]---> BDD-cost: 76 c ---[ 213]---> BDD-cost: 76 c ---[ 211]---> BDD-cost: 76 c ---[ 209]---> BDD-cost: 76 c ---[ 207]---> BDD-cost: 76 c ---[ 205]---> BDD-cost: 76 c ---[ 203]---> BDD-cost: 76 c ---[ 201]---> BDD-cost: 76 c ---[ 199]---> BDD-cost: 76 c ---[ 197]---> BDD-cost: 76 c ---[ 195]---> BDD-cost: 76 c ---[ 193]---> BDD-cost: 76 c ---[ 191]---> BDD-cost: 76 c ---[ 189]---> BDD-cost: 76 c ---[ 187]---> BDD-cost: 76 c ---[ 185]---> BDD-cost: 76 c ---[ 183]---> BDD-cost: 76 c ---[ 181]---> BDD-cost: 76 c ---[ 179]---> BDD-cost: 76 c ---[ 177]---> BDD-cost: 76 c ---[ 175]---> BDD-cost: 76 c ---[ 173]---> BDD-cost: 76 c ---[ 171]---> BDD-cost: 76 c ---[ 169]---> BDD-cost: 76 c ---[ 167]---> BDD-cost: 76 c ---[ 165]---> BDD-cost: 35 c ---[ 163]---> BDD-cost: 76 c ---[ 161]---> BDD-cost: 76 c ---[ 159]---> BDD-cost: 76 c ---[ 157]---> BDD-cost: 76 c ---[ 155]---> BDD-cost: 76 c ---[ 153]---> BDD-cost: 76 c ---[ 151]---> BDD-cost: 76 c ---[ 149]---> BDD-cost: 76 c ---[ 147]---> BDD-cost: 76 c ---[ 145]---> BDD-cost: 76 c ---[ 143]---> BDD-cost: 76 c ---[ 141]---> BDD-cost: 76 c ---[ 139]---> BDD-cost: 76 c ---[ 137]---> BDD-cost: 76 c ---[ 135]---> BDD-cost: 76 c ---[ 133]---> BDD-cost: 76 c ---[ 131]---> BDD-cost: 76 c ---[ 129]---> BDD-cost: 76 c ---[ 127]---> BDD-cost: 76 c ---[ 125]---> BDD-cost: 76 c ---[ 123]---> BDD-cost: 76 c ---[ 121]---> BDD-cost: 76 c ---[ 119]---> BDD-cost: 76 c ---[ 117]---> BDD-cost: 76 c ---[ 115]---> BDD-cost: 76 c ---[ 113]---> BDD-cost: 76 c ---[ 111]---> BDD-cost: 35 c ---[ 109]---> BDD-cost: 76 c ---[ 107]---> BDD-cost: 76 c ---[ 105]---> BDD-cost: 76 c ---[ 103]---> BDD-cost: 76 c ---[ 101]---> BDD-cost: 76 c ---[ 99]---> BDD-cost: 76 c ---[ 97]---> BDD-cost: 76 c ---[ 95]---> BDD-cost: 76 c ---[ 93]---> BDD-cost: 76 c ---[ 91]---> BDD-cost: 76 c ---[ 89]---> BDD-cost: 76 c ---[ 87]---> BDD-cost: 76 c ---[ 85]---> BDD-cost: 76 c ---[ 83]---> BDD-cost: 76 c ---[ 81]---> BDD-cost: 76 c ---[ 79]---> BDD-cost: 76 c ---[ 77]---> BDD-cost: 76 c ---[ 75]---> BDD-cost: 76 c ---[ 73]---> BDD-cost: 76 c ---[ 71]---> BDD-cost: 76 c ---[ 69]---> BDD-cost: 76 c ---[ 67]---> BDD-cost: 76 c ---[ 65]---> BDD-cost: 76 c ---[ 63]---> BDD-cost: 76 c ---[ 61]---> BDD-cost: 76 c ---[ 59]---> BDD-cost: 76 c ---[ 57]---> BDD-cost: 76 c ---[ 55]---> BDD-cost: 76 c ---[ 53]---> BDD-cost: 76 c ---[ 51]---> BDD-cost: 76 c ---[ 49]---> BDD-cost: 76 c ---[ 47]---> BDD-cost: 76 c ---[ 45]---> BDD-cost: 76 c ---[ 43]---> BDD-cost: 76 c ---[ 41]---> BDD-cost: 76 c ---[ 39]---> BDD-cost: 76 c ---[ 37]---> BDD-cost: 76 c ---[ 35]---> BDD-cost: 76 c ---[ 33]---> BDD-cost: 76 c ---[ 31]---> BDD-cost: 35 c ---[ 29]---> BDD-cost: 35 c ---[ 27]---> BDD-cost: 76 c ---[ 25]---> BDD-cost: 76 c ---[ 23]---> BDD-cost: 76 c ---[ 21]---> BDD-cost: 76 c ---[ 19]---> BDD-cost: 76 c ---[ 17]---> BDD-cost: 76 c ---[ 15]---> BDD-cost: 76 c ---[ 13]---> BDD-cost: 76 c ---[ 11]---> BDD-cost: 76 c ---[ 9]---> BDD-cost: 76 c ---[ 7]---> BDD-cost: 76 c ---[ 5]---> BDD-cost: 76 c ---[ 3]---> BDD-cost: 76 c ---[ 2]---> BDD-cost: 20 c ---[ 1]---> BDD-cost: 20 c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 2410614 7168880 | 803538 0 0 nan | 0.000 % | c | 101 | 2410614 7168880 | 883891 101 10956 108.5 | 0.786 % | c | 251 | 2410614 7168880 | 972280 251 21407 85.3 | 0.786 % | c | 476 | 2410614 7168880 | 1069509 476 40969 86.1 | 0.786 % | c | 813 | 2410614 7168880 | 1176459 813 93260 114.7 | 0.786 % | c | 1320 | 2410614 7168880 | 1294105 1320 127714 96.8 | 0.786 % | c | 2079 | 2410614 7168880 | 1423516 2079 156326 75.2 | 0.786 % | c | 3218 | 2410614 7168880 | 1565868 3218 449961 139.8 | 0.786 % | c | 4927 | 2410614 7168880 | 1722455 4927 598838 121.5 | 0.786 % | c | 7489 | 2410614 7168880 | 1894700 7489 881743 117.7 | 0.786 % | c | 11333 | 2410614 7168880 | 2084170 11333 1519724 134.1 | 0.786 % | c | 17100 | 2410614 7168880 | 2292587 17100 2336554 136.6 | 0.786 % | c | 25750 | 2410614 7168880 | 2521846 25750 4604678 178.8 | 0.786 % | c | 38724 | 2410614 7168880 | 2774031 38724 5233095 135.1 | 0.786 % | c | 58187 | 2410614 7168880 | 3051434 58187 6094545 104.7 | 0.786 % | c | 87379 | 2410614 7168880 | 3356577 87379 9881553 113.1 | 0.786 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.93 0.98 0.93 2/54 30792 Raw data (stat): 30792 (runsolver) R 30791 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547807908 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0009 s] Raw data (loadavg): 0.94 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 42064 0 0 0 900 99 0 0 25 0 1 0 547807908 176091136 37798 4294967295 134512640 134672761 3221224544 3221153920 1075349701 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 42991 37798 603 41 0 42950 0 vsize: 171964 [startup+20.0011 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75135 0 0 0 1820 179 0 0 25 0 1 0 547807908 322052096 70869 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78626 70869 603 41 0 78585 0 vsize: 314504 [startup+30.0017 s] Raw data (loadavg): 0.96 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75211 0 0 0 2820 179 0 0 25 0 1 0 547807908 322457600 70945 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78725 70945 603 41 0 78684 0 vsize: 314900 [startup+40.0018 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75247 0 0 0 3819 180 0 0 25 0 1 0 547807908 322592768 70981 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78758 70981 603 41 0 78717 0 vsize: 315032 [startup+50.0021 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75712 0 0 0 4818 181 0 0 25 0 1 0 547807908 323678208 71446 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79023 71446 603 41 0 78982 0 vsize: 316092 [startup+60.0028 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75814 0 0 0 5818 182 0 0 25 0 1 0 547807908 324083712 71548 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79122 71548 603 41 0 79081 0 vsize: 316488 [startup+70.0038 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75877 0 0 0 6817 182 0 0 25 0 1 0 547807908 324354048 71611 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79188 71611 603 41 0 79147 0 vsize: 316752 [startup+80.0042 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75929 0 0 0 7817 183 0 0 25 0 1 0 547807908 324485120 71663 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79220 71663 603 41 0 79179 0 vsize: 316880 [startup+90.0038 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75984 0 0 0 8817 183 0 0 25 0 1 0 547807908 324755456 71718 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79286 71718 603 41 0 79245 0 vsize: 317144 [startup+100.004 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76052 0 0 0 9817 184 0 0 25 0 1 0 547807908 325021696 71786 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79351 71786 603 41 0 79310 0 vsize: 317404 [startup+110.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76144 0 0 0 10816 184 0 0 25 0 1 0 547807908 325419008 71878 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79448 71878 603 41 0 79407 0 vsize: 317792 [startup+120.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76223 0 0 0 11816 185 0 0 25 0 1 0 547807908 325685248 71957 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79513 71957 603 41 0 79472 0 vsize: 318052 [startup+130.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76290 0 0 0 12816 185 0 0 25 0 1 0 547807908 325951488 72024 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79578 72024 603 41 0 79537 0 vsize: 318312 [startup+140.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76358 0 0 0 13815 185 0 0 25 0 1 0 547807908 326348800 72092 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79675 72092 603 41 0 79634 0 vsize: 318700 [startup+150.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76423 0 0 0 14815 186 0 0 25 0 1 0 547807908 326615040 72157 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79740 72157 603 41 0 79699 0 vsize: 318960 [startup+160.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76508 0 0 0 15815 186 0 0 25 0 1 0 547807908 326885376 72242 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79806 72242 603 41 0 79765 0 vsize: 319224 [startup+170.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76578 0 0 0 16814 187 0 0 25 0 1 0 547807908 327208960 72312 4294967295 134512640 134672761 3221224544 3221223728 134559293 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79885 72312 603 41 0 79844 0 vsize: 319540 [startup+180.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76619 0 0 0 17814 187 0 0 25 0 1 0 547807908 327340032 72353 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79917 72353 603 41 0 79876 0 vsize: 319668 [startup+190.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76668 0 0 0 18814 188 0 0 25 0 1 0 547807908 327659520 72402 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 79995 72402 603 41 0 79954 0 vsize: 319980 [startup+200.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76706 0 0 0 19814 188 0 0 25 0 1 0 547807908 327794688 72440 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 80028 72440 603 41 0 79987 0 vsize: 320112 [startup+210.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76747 0 0 0 20813 189 0 0 25 0 1 0 547807908 327929856 72481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80061 72481 603 41 0 80020 0 vsize: 320244 [startup+220.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76791 0 0 0 21813 189 0 0 25 0 1 0 547807908 328060928 72525 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80093 72525 603 41 0 80052 0 vsize: 320372 [startup+230.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76838 0 0 0 22814 189 0 0 25 0 1 0 547807908 328331264 72572 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80159 72572 603 41 0 80118 0 vsize: 320636 [startup+240.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76880 0 0 0 23813 189 0 0 25 0 1 0 547807908 328462336 72614 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80191 72614 603 41 0 80150 0 vsize: 320764 [startup+250.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30792 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76921 0 0 0 24813 189 0 0 25 0 1 0 547807908 328593408 72655 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80223 72655 603 41 0 80182 0 vsize: 320892 [startup+260.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76966 0 0 0 25813 189 0 0 25 0 1 0 547807908 328863744 72700 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80289 72700 603 41 0 80248 0 vsize: 321156 [startup+270.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77008 0 0 0 26814 189 0 0 25 0 1 0 547807908 328998912 72742 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80322 72742 603 41 0 80281 0 vsize: 321288 [startup+280.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77053 0 0 0 27813 190 0 0 25 0 1 0 547807908 329134080 72787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80355 72787 603 41 0 80314 0 vsize: 321420 [startup+290.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77092 0 0 0 28814 190 0 0 25 0 1 0 547807908 329269248 72826 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80388 72826 603 41 0 80347 0 vsize: 321552 [startup+300.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77142 0 0 0 29813 190 0 0 25 0 1 0 547807908 329539584 72876 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80454 72876 603 41 0 80413 0 vsize: 321816 [startup+310.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77183 0 0 0 30813 191 0 0 25 0 1 0 547807908 329670656 72917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80486 72917 603 41 0 80445 0 vsize: 321944 [startup+320.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77220 0 0 0 31813 191 0 0 25 0 1 0 547807908 329801728 72954 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 80518 72954 603 41 0 80477 0 vsize: 322072 [startup+330.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77440 0 0 0 32812 192 0 0 25 0 1 0 547807908 330747904 73174 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80749 73174 603 41 0 80708 0 vsize: 322996 [startup+340.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77648 0 0 0 33811 192 0 0 25 0 1 0 547807908 331558912 73382 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80947 73382 603 41 0 80906 0 vsize: 323788 [startup+350.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77809 0 0 0 34811 193 0 0 25 0 1 0 547807908 332230656 73543 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 81111 73543 603 41 0 81070 0 vsize: 324444 [startup+360.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78057 0 0 0 35810 194 0 0 25 0 1 0 547807908 333312000 73791 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 81375 73791 603 41 0 81334 0 vsize: 325500 [startup+370.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78187 0 0 0 36810 194 0 0 25 0 1 0 547807908 333852672 73921 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 81507 73921 603 41 0 81466 0 vsize: 326028 [startup+380.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78308 0 0 0 37810 194 0 0 25 0 1 0 547807908 334393344 74042 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 81639 74042 603 41 0 81598 0 vsize: 326556 [startup+390.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78436 0 0 0 38809 195 0 0 25 0 1 0 547807908 334798848 74170 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 81738 74170 603 41 0 81697 0 vsize: 326952 [startup+400.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78552 0 0 0 39809 195 0 0 25 0 1 0 547807908 335335424 74286 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 81869 74286 603 41 0 81828 0 vsize: 327476 [startup+410.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78635 0 0 0 40809 195 0 0 25 0 1 0 547807908 335605760 74369 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 81935 74369 603 41 0 81894 0 vsize: 327740 [startup+420.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78774 0 0 0 41809 196 0 0 25 0 1 0 547807908 336273408 74508 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82098 74508 603 41 0 82057 0 vsize: 328392 [startup+430.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78890 0 0 0 42809 196 0 0 25 0 1 0 547807908 336670720 74624 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82195 74624 603 41 0 82154 0 vsize: 328780 [startup+440.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78978 0 0 0 43809 196 0 0 25 0 1 0 547807908 337072128 74712 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82293 74712 603 41 0 82252 0 vsize: 329172 [startup+450.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79046 0 0 0 44809 197 0 0 25 0 1 0 547807908 337338368 74780 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82358 74780 603 41 0 82317 0 vsize: 329432 [startup+460.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79106 0 0 0 45809 197 0 0 25 0 1 0 547807908 337608704 74840 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82424 74840 603 41 0 82383 0 vsize: 329696 [startup+470.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79239 0 0 0 46809 197 0 0 25 0 1 0 547807908 338149376 74973 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82556 74973 603 41 0 82515 0 vsize: 330224 [startup+480.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79350 0 0 0 47809 197 0 0 25 0 1 0 547807908 338554880 75084 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82655 75084 603 41 0 82614 0 vsize: 330620 [startup+490.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79461 0 0 0 48809 198 0 0 25 0 1 0 547807908 339087360 75195 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82785 75195 603 41 0 82744 0 vsize: 331140 [startup+500.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79565 0 0 0 49809 198 0 0 25 0 1 0 547807908 339484672 75299 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82882 75299 603 41 0 82841 0 vsize: 331528 [startup+510.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79666 0 0 0 50808 198 0 0 25 0 1 0 547807908 339881984 75400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82979 75400 603 41 0 82938 0 vsize: 331916 [startup+520.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79809 0 0 0 51808 199 0 0 25 0 1 0 547807908 340418560 75543 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83110 75543 603 41 0 83069 0 vsize: 332440 [startup+530.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79915 0 0 0 52808 199 0 0 25 0 1 0 547807908 340959232 75649 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83242 75649 603 41 0 83201 0 vsize: 332968 [startup+540.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80017 0 0 0 53808 199 0 0 25 0 1 0 547807908 341364736 75751 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83341 75751 603 41 0 83300 0 vsize: 333364 [startup+550.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80133 0 0 0 54808 199 0 0 25 0 1 0 547807908 341774336 75867 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83441 75867 603 41 0 83400 0 vsize: 333764 [startup+560.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80217 0 0 0 55808 200 0 0 25 0 1 0 547807908 342175744 75951 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83539 75951 603 41 0 83498 0 vsize: 334156 [startup+570.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80322 0 0 0 56808 200 0 0 25 0 1 0 547807908 342577152 76056 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83637 76056 603 41 0 83596 0 vsize: 334548 [startup+580.019 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80412 0 0 0 57808 200 0 0 25 0 1 0 547807908 342974464 76146 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 83734 76146 603 41 0 83693 0 vsize: 334936 [startup+590.019 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80468 0 0 0 58808 201 0 0 25 0 1 0 547807908 343105536 76202 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83766 76202 603 41 0 83725 0 vsize: 335064 [startup+600.019 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80533 0 0 0 59808 201 0 0 25 0 1 0 547807908 343367680 76267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83830 76267 603 41 0 83789 0 vsize: 335320 [startup+610.019 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80592 0 0 0 60808 201 0 0 25 0 1 0 547807908 343629824 76326 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83894 76326 603 41 0 83853 0 vsize: 335576 [startup+620.018 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80661 0 0 0 61808 201 0 0 25 0 1 0 547807908 343896064 76395 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83959 76395 603 41 0 83918 0 vsize: 335836 [startup+630.018 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80734 0 0 0 62808 201 0 0 25 0 1 0 547807908 344293376 76468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84056 76468 603 41 0 84015 0 vsize: 336224 [startup+640.018 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80789 0 0 0 63808 201 0 0 25 0 1 0 547807908 344424448 76523 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84088 76523 603 41 0 84047 0 vsize: 336352 [startup+650.017 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80845 0 0 0 64808 202 0 0 25 0 1 0 547807908 344817664 76579 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84184 76579 603 41 0 84143 0 vsize: 336736 [startup+660.017 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80901 0 0 0 65808 202 0 0 25 0 1 0 547807908 345083904 76635 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84249 76635 603 41 0 84208 0 vsize: 336996 [startup+670.017 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80958 0 0 0 66808 202 0 0 25 0 1 0 547807908 345214976 76692 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84281 76692 603 41 0 84240 0 vsize: 337124 [startup+680.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81014 0 0 0 67808 202 0 0 25 0 1 0 547807908 345477120 76748 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84345 76748 603 41 0 84304 0 vsize: 337380 [startup+690.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81079 0 0 0 68808 202 0 0 25 0 1 0 547807908 345739264 76813 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84409 76813 603 41 0 84368 0 vsize: 337636 [startup+700.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81149 0 0 0 69808 202 0 0 25 0 1 0 547807908 346025984 76883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84479 76883 603 41 0 84438 0 vsize: 337916 [startup+710.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81220 0 0 0 70808 203 0 0 25 0 1 0 547807908 346292224 76954 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84544 76954 603 41 0 84503 0 vsize: 338176 [startup+720.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81272 0 0 0 71808 203 0 0 25 0 1 0 547807908 346558464 77006 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84609 77006 603 41 0 84568 0 vsize: 338436 [startup+730.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81324 0 0 0 72808 203 0 0 25 0 1 0 547807908 346689536 77058 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84641 77058 603 41 0 84600 0 vsize: 338564 [startup+740.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81382 0 0 0 73808 204 0 0 25 0 1 0 547807908 346951680 77116 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84705 77116 603 41 0 84664 0 vsize: 338820 [startup+750.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81443 0 0 0 74808 204 0 0 25 0 1 0 547807908 347213824 77177 4294967295 134512640 134672761 3221224544 3221223648 134555175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84769 77177 603 41 0 84728 0 vsize: 339076 [startup+760.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81490 0 0 0 75808 204 0 0 25 0 1 0 547807908 347480064 77224 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84834 77224 603 41 0 84793 0 vsize: 339336 [startup+770.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81543 0 0 0 76808 204 0 0 25 0 1 0 547807908 347611136 77277 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84866 77277 603 41 0 84825 0 vsize: 339464 [startup+780.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81598 0 0 0 77808 204 0 0 25 0 1 0 547807908 347877376 77332 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84931 77332 603 41 0 84890 0 vsize: 339724 [startup+790.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81646 0 0 0 78808 204 0 0 25 0 1 0 547807908 348008448 77380 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84963 77380 603 41 0 84922 0 vsize: 339852 [startup+800.022 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81710 0 0 0 79808 204 0 0 25 0 1 0 547807908 348278784 77444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85029 77444 603 41 0 84988 0 vsize: 340116 [startup+810.022 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81766 0 0 0 80808 205 0 0 25 0 1 0 547807908 348549120 77500 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85095 77500 603 41 0 85054 0 vsize: 340380 [startup+820.022 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81813 0 0 0 81808 205 0 0 25 0 1 0 547807908 348680192 77547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85127 77547 603 41 0 85086 0 vsize: 340508 [startup+830.032 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81883 0 0 0 82809 205 0 0 25 0 1 0 547807908 349077504 77617 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85224 77617 603 41 0 85183 0 vsize: 340896 [startup+840.037 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81972 0 0 0 83810 205 0 0 25 0 1 0 547807908 349339648 77706 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85288 77706 603 41 0 85247 0 vsize: 341152 [startup+850.037 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82048 0 0 0 84810 205 0 0 25 0 1 0 547807908 349736960 77782 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85385 77782 603 41 0 85344 0 vsize: 341540 [startup+860.052 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82127 0 0 0 85811 205 0 0 25 0 1 0 547807908 349999104 77861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85449 77861 603 41 0 85408 0 vsize: 341796 [startup+870.067 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82186 0 0 0 86812 206 0 0 25 0 1 0 547807908 350261248 77920 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85513 77920 603 41 0 85472 0 vsize: 342052 [startup+880.067 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82256 0 0 0 87812 206 0 0 25 0 1 0 547807908 350531584 77990 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85579 77990 603 41 0 85538 0 vsize: 342316 [startup+890.068 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82355 0 0 0 88812 206 0 0 25 0 1 0 547807908 350937088 78089 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85678 78089 603 41 0 85637 0 vsize: 342712 [startup+900.067 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82466 0 0 0 89812 207 0 0 25 0 1 0 547807908 351334400 78200 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85775 78200 603 41 0 85734 0 vsize: 343100 [startup+910.076 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82556 0 0 0 90812 207 0 0 25 0 1 0 547807908 351735808 78290 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85873 78290 603 41 0 85832 0 vsize: 343492 [startup+920.076 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82634 0 0 0 91812 208 0 0 25 0 1 0 547807908 352006144 78368 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85939 78368 603 41 0 85898 0 vsize: 343756 [startup+930.075 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82711 0 0 0 92811 208 0 0 25 0 1 0 547807908 352399360 78445 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86035 78445 603 41 0 85994 0 vsize: 344140 [startup+940.076 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82764 0 0 0 93812 208 0 0 25 0 1 0 547807908 352534528 78498 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86068 78498 603 41 0 86027 0 vsize: 344272 [startup+950.076 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82831 0 0 0 94811 209 0 0 25 0 1 0 547807908 352800768 78565 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86133 78565 603 41 0 86092 0 vsize: 344532 [startup+960.075 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82902 0 0 0 95811 209 0 0 25 0 1 0 547807908 353202176 78636 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86231 78636 603 41 0 86190 0 vsize: 344924 [startup+970.075 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82988 0 0 0 96811 209 0 0 25 0 1 0 547807908 353468416 78722 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86296 78722 603 41 0 86255 0 vsize: 345184 [startup+980.075 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83069 0 0 0 97811 209 0 0 25 0 1 0 547807908 353865728 78803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86393 78803 603 41 0 86352 0 vsize: 345572 [startup+990.074 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83142 0 0 0 98811 209 0 0 25 0 1 0 547807908 354136064 78876 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86459 78876 603 41 0 86418 0 vsize: 345836 [startup+1000.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83221 0 0 0 99811 210 0 0 25 0 1 0 547807908 354668544 78955 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86589 78955 603 41 0 86548 0 vsize: 346356 [startup+1010.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83311 0 0 0 100811 210 0 0 25 0 1 0 547807908 355069952 79045 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86687 79045 603 41 0 86646 0 vsize: 346748 [startup+1020.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83482 0 0 0 101811 211 0 0 25 0 1 0 547807908 355741696 79216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86851 79216 603 41 0 86810 0 vsize: 347404 [startup+1030.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83681 0 0 0 102810 211 0 0 25 0 1 0 547807908 356544512 79415 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 87047 79415 603 41 0 87006 0 vsize: 348188 [startup+1040.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83793 0 0 0 103810 212 0 0 25 0 1 0 547807908 357081088 79527 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 87178 79527 603 41 0 87137 0 vsize: 348712 [startup+1050.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 84162 0 0 0 104809 213 0 0 25 0 1 0 547807908 358563840 79896 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 87540 79896 603 41 0 87499 0 vsize: 350160 [startup+1060.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 84524 0 0 0 105808 214 0 0 25 0 1 0 547807908 360042496 80258 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 87901 80258 603 41 0 87860 0 vsize: 351604 [startup+1070.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 84873 0 0 0 106807 215 0 0 25 0 1 0 547807908 361385984 80607 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 88229 80607 603 41 0 88188 0 vsize: 352916 [startup+1080.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 85127 0 0 0 107807 216 0 0 25 0 1 0 547807908 362459136 80861 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 88491 80861 603 41 0 88450 0 vsize: 353964 [startup+1090.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 85392 0 0 0 108806 217 0 0 25 0 1 0 547807908 363540480 81126 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 88755 81126 603 41 0 88714 0 vsize: 355020 [startup+1100.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 85680 0 0 0 109805 218 0 0 25 0 1 0 547807908 364773376 81414 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 89056 81414 603 41 0 89015 0 vsize: 356224 [startup+1110.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86050 0 0 0 110803 219 0 0 25 0 1 0 547807908 366272512 81784 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 89422 81784 603 41 0 89381 0 vsize: 357688 [startup+1120.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86334 0 0 0 111802 220 0 0 25 0 1 0 547807908 367484928 82068 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 89718 82068 603 41 0 89677 0 vsize: 358872 [startup+1130.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86498 0 0 0 112801 221 0 0 25 0 1 0 547807908 368160768 82232 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 89883 82232 603 41 0 89842 0 vsize: 359532 [startup+1140.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86618 0 0 0 113800 222 0 0 25 0 1 0 547807908 368562176 82352 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 89981 82352 603 41 0 89940 0 vsize: 359924 [startup+1150.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86726 0 0 0 114799 223 0 0 25 0 1 0 547807908 369102848 82460 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 90113 82460 603 41 0 90072 0 vsize: 360452 [startup+1160.08 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86820 0 0 0 115799 223 0 0 25 0 1 0 547807908 369373184 82554 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 90179 82554 603 41 0 90138 0 vsize: 360716 [startup+1170.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86873 0 0 0 116799 223 0 0 25 0 1 0 547807908 369643520 82607 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 90245 82607 603 41 0 90204 0 vsize: 360980 [startup+1180.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86917 0 0 0 117799 223 0 0 25 0 1 0 547807908 369778688 82651 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 90278 82651 603 41 0 90237 0 vsize: 361112 [startup+1190.08 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86970 0 0 0 118799 223 0 0 25 0 1 0 547807908 370049024 82704 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 90344 82704 603 41 0 90303 0 vsize: 361376 [startup+1200.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30794 Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 87039 0 0 0 119799 224 0 0 25 0 1 0 547807908 370319360 82773 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 90410 82773 603 41 0 90369 0 vsize: 361640 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.24 s] Raw data (loadavg): 0.99 0.98 0.93 1/54 30794 Raw data (stat): 30792 (minisat+) Z 30791 10614 10613 0 -1 12 87041 0 0 0 119799 240 0 0 25 0 1 0 547807908 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.24 CPU time (s): 1200.4 CPU user time (s): 1197.99 CPU system time (s): 2.40363 CPU usage (%): 100.013 Max. virtual memory (Kb): 361640 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####