Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-degen2.opb |
MD5SUM | 2d6764e721075c7867e38358b7c5ac96 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 14100 |
Biggest coefficient in the objective function | 2553894928384 |
Number of bits for the biggest coefficient in the objective function | 42 |
Sum of the numbers in the objective function | 401268056673330 |
Number of bits of the sum of numbers in the objective function | 49 |
Biggest number in a constraint | 2553894928384 |
Number of bits of the biggest number in a constraint | 42 |
Biggest sum of numbers in a constraint | 401268056673330 |
Number of bits of the biggest sum of numbers | 49 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 16020 |
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 | 60 |
Maximum length of a constraint | 2550 |
LAUNCH ON wulflinc15 THE 2005-09-18 20:15:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2766 boxname=wulflinc15 idbench=422 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 2d6764e721075c7867e38358b7c5ac96 /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-degen2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-degen2.opb IDLAUNCH: 2766 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 912216 kB Buffers: 33836 kB Cached: 59312 kB SwapCached: 692 kB Active: 57684 kB Inactive: 38076 kB HighTotal: 131008 kB HighFree: 68516 kB LowTotal: 903652 kB LowFree: 843700 kB SwapTotal: 2097136 kB SwapFree: 2095920 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 20828 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 20:35:23 (client local time) WITH STATUS 0 IN 1207.6 SECONDS stats: 2766 7 1207.6 0
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]---> Adder-cost: 2006 maxlim: 1460142 bits: 21/21 c ---[ 666]---> Adder-cost: 2018 maxlim: 829356 bits: 20/20 c ---[ 665]---> Adder-cost: 1546 maxlim: 721857 bits: 20/20 c ---[ 663]---> Adder-cost: 242 maxlim: 12282 bits: 15/14 c ---[ 661]---> Adder-cost: 242 maxlim: 12282 bits: 15/14 c ---[ 659]---> Adder-cost: 352 maxlim: 17399 bits: 16/15 c ---[ 657]---> Adder-cost: 352 maxlim: 18423 bits: 16/15 c ---[ 655]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 653]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 651]---> Sorter-cost: 2089 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 649]---> Sorter-cost: 2089 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 647]---> Adder-cost: 682 maxlim: 34799 bits: 16/16 c ---[ 645]---> Adder-cost: 726 maxlim: 34799 bits: 17/16 c ---[ 643]---> Sorter-cost: 2089 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 641]---> Sorter-cost: 2089 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 639]---> Adder-cost: 440 maxlim: 22517 bits: 16/15 c ---[ 637]---> Adder-cost: 440 maxlim: 22517 bits: 16/15 c ---[ 635]---> Sorter-cost: 1322 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 633]---> Sorter-cost: 1322 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 631]---> Adder-cost: 440 maxlim: 22517 bits: 16/15 c ---[ 629]---> Adder-cost: 462 maxlim: 22517 bits: 16/15 c ---[ 627]---> BDD-cost: 31 c ---[ 625]---> Adder-cost: 286 maxlim: 14329 bits: 15/14 c ---[ 623]---> Adder-cost: 286 maxlim: 14329 bits: 15/14 c ---[ 621]---> Adder-cost: 869 maxlim: 41964 bits: 17/16 c ---[ 619]---> Adder-cost: 825 maxlim: 38893 bits: 17/16 c ---[ 617]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 615]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 613]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 611]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 609]---> Adder-cost: 1144 maxlim: 51175 bits: 17/16 c ---[ 607]---> Adder-cost: 1166 maxlim: 54246 bits: 17/16 c ---[ 605]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 603]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 601]---> Adder-cost: 242 maxlim: 12282 bits: 15/14 c ---[ 599]---> Adder-cost: 242 maxlim: 12282 bits: 15/14 c ---[ 597]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 595]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 593]---> Sorter-cost: 400 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 591]---> Sorter-cost: 400 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 589]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 587]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 585]---> Adder-cost: 330 maxlim: 16376 bits: 15/14 c ---[ 583]---> Adder-cost: 308 maxlim: 16376 bits: 15/14 c ---[ 581]---> Adder-cost: 638 maxlim: 30705 bits: 16/15 c ---[ 579]---> Adder-cost: 660 maxlim: 32752 bits: 16/15 c ---[ 577]---> BDD-cost: 91 c ---[ 576]---> Sorter-cost: 431 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 575]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 574]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 573]---> Sorter-cost: 882 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 572]---> Sorter-cost: 968 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 571]---> Sorter-cost: 968 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 570]---> Sorter-cost: 1300 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 569]---> Sorter-cost: 1392 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 568]---> Sorter-cost: 1392 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 567]---> BDD-cost: 35 c ---[ 566]---> Sorter-cost: 431 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 565]---> BDD-cost: 94 c ---[ 564]---> BDD-cost: 94 c ---[ 563]---> Sorter-cost: 1300 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 562]---> Sorter-cost: 1260 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 561]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 560]---> Sorter-cost: 2273 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 559]---> Sorter-cost: 1846 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 558]---> BDD-cost: 95 c ---[ 557]---> BDD-cost: 94 c ---[ 556]---> BDD-cost: 94 c ---[ 555]---> BDD-cost: 95 c ---[ 554]---> BDD-cost: 94 c ---[ 553]---> BDD-cost: 94 c ---[ 552]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 551]---> Sorter-cost: 559 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 550]---> Sorter-cost: 669 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 549]---> Sorter-cost: 1019 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 548]---> Sorter-cost: 1129 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 547]---> Sorter-cost: 1151 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 546]---> Sorter-cost: 1153 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 545]---> Sorter-cost: 1263 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 544]---> Sorter-cost: 1263 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 543]---> Adder-cost: 227 maxlim: 12281 bits: 15/14 c ---[ 542]---> Adder-cost: 226 maxlim: 11257 bits: 15/14 c ---[ 541]---> Adder-cost: 226 maxlim: 12281 bits: 15/14 c ---[ 540]---> Adder-cost: 295 maxlim: 16375 bits: 15/14 c ---[ 539]---> Adder-cost: 314 maxlim: 15351 bits: 15/14 c ---[ 538]---> Adder-cost: 314 maxlim: 16375 bits: 15/14 c ---[ 537]---> Adder-cost: 295 maxlim: 18422 bits: 16/15 c ---[ 536]---> Adder-cost: 308 maxlim: 17398 bits: 16/15 c ---[ 535]---> Adder-cost: 330 maxlim: 18422 bits: 16/15 c ---[ 534]---> Adder-cost: 358 maxlim: 24563 bits: 16/15 c ---[ 533]---> Adder-cost: 403 maxlim: 23539 bits: 16/15 c ---[ 532]---> Adder-cost: 425 maxlim: 24563 bits: 16/15 c ---[ 531]---> Adder-cost: 472 maxlim: 26610 bits: 16/15 c ---[ 530]---> Adder-cost: 493 maxlim: 25586 bits: 16/15 c ---[ 529]---> Adder-cost: 493 maxlim: 26610 bits: 16/15 c ---[ 528]---> Adder-cost: 472 maxlim: 28657 bits: 16/15 c ---[ 527]---> Adder-cost: 515 maxlim: 27633 bits: 16/15 c ---[ 526]---> Adder-cost: 537 maxlim: 28657 bits: 16/15 c ---[ 525]---> Adder-cost: 412 maxlim: 30704 bits: 16/15 c ---[ 524]---> Adder-cost: 443 maxlim: 29680 bits: 16/15 c ---[ 523]---> Adder-cost: 555 maxlim: 30704 bits: 16/15 c ---[ 522]---> BDD-cost: 95 c ---[ 521]---> BDD-cost: 94 c ---[ 520]---> BDD-cost: 94 c ---[ 519]---> Sorter-cost: 651 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 518]---> Sorter-cost: 647 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 517]---> Sorter-cost: 669 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 516]---> Sorter-cost: 1129 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 515]---> Sorter-cost: 1239 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 514]---> Sorter-cost: 1261 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 513]---> Sorter-cost: 926 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 512]---> Sorter-cost: 1012 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 511]---> Sorter-cost: 1390 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 510]---> Sorter-cost: 1483 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 509]---> BDD-cost: 94 c ---[ 508]---> Sorter-cost: 669 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 507]---> Adder-cost: 227 maxlim: 14328 bits: 15/14 c ---[ 506]---> Sorter-cost: 2456 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 505]---> Sorter-cost: 1012 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 504]---> Adder-cost: 271 maxlim: 18422 bits: 16/15 c ---[ 503]---> Adder-cost: 292 maxlim: 18422 bits: 16/15 c ---[ 502]---> Sorter-cost: 1457 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 501]---> Adder-cost: 309 maxlim: 20469 bits: 16/15 c ---[ 500]---> Adder-cost: 330 maxlim: 20469 bits: 16/15 c ---[ 499]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 498]---> Sorter-cost: 559 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 497]---> BDD-cost: 95 c ---[ 496]---> BDD-cost: 94 c ---[ 495]---> Sorter-cost: 1863 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 494]---> Sorter-cost: 1920 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 493]---> Adder-cost: 251 maxlim: 10234 bits: 15/14 c ---[ 492]---> Adder-cost: 268 maxlim: 10234 bits: 15/14 c ---[ 491]---> Sorter-cost: 428 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 490]---> BDD-cost: 95 c ---[ 489]---> BDD-cost: 94 c ---[ 488]---> BDD-cost: 94 c ---[ 487]---> Sorter-cost: 649 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 486]---> Sorter-cost: 645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 485]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> Sorter-cost: 1151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 483]---> Sorter-cost: 1261 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 482]---> Sorter-cost: 1261 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 481]---> Sorter-cost: 1729 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 480]---> Sorter-cost: 1780 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 479]---> Sorter-cost: 1780 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 478]---> Adder-cost: 183 maxlim: 10234 bits: 15/14 c ---[ 477]---> Sorter-cost: 2419 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 476]---> Sorter-cost: 2419 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 475]---> Sorter-cost: 432 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 474]---> Sorter-cost: 428 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 473]---> Sorter-cost: 1389 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 472]---> Sorter-cost: 1481 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 471]---> Adder-cost: 203 maxlim: 6140 bits: 14/13 c ---[ 470]---> BDD-cost: 94 c ---[ 469]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 468]---> Adder-cost: 339 maxlim: 14328 bits: 15/14 c ---[ 467]---> Adder-cost: 314 maxlim: 13305 bits: 15/14 c ---[ 466]---> Adder-cost: 288 maxlim: 16375 bits: 15/14 c ---[ 465]---> Adder-cost: 284 maxlim: 15352 bits: 15/14 c ---[ 464]---> Sorter-cost: 1239 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 463]---> Adder-cost: 405 maxlim: 17399 bits: 16/15 c ---[ 462]---> Adder-cost: 402 maxlim: 19446 bits: 16/15 c ---[ 461]---> Adder-cost: 388 maxlim: 21493 bits: 16/15 c ---[ 460]---> Adder-cost: 365 maxlim: 19446 bits: 16/15 c ---[ 459]---> Sorter-cost: 2220 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 458]---> Adder-cost: 582 maxlim: 22516 bits: 16/15 c ---[ 457]---> Adder-cost: 624 maxlim: 25586 bits: 16/15 c ---[ 456]---> Adder-cost: 601 maxlim: 24563 bits: 16/15 c ---[ 455]---> BDD-cost: 93 c ---[ 454]---> BDD-cost: 92 c ---[ 453]---> BDD-cost: 94 c ---[ 452]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 451]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 450]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 449]---> BDD-cost: 34 c ---[ 448]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 447]---> BDD-cost: 95 c ---[ 446]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 445]---> Sorter-cost: 968 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 442]---> Sorter-cost: 674 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 441]---> Sorter-cost: 670 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 440]---> Sorter-cost: 428 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 439]---> Adder-cost: 250 maxlim: 15352 bits: 15/14 c ---[ 438]---> Sorter-cost: 2244 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 437]---> Adder-cost: 251 maxlim: 15352 bits: 15/14 c ---[ 436]---> Adder-cost: 272 maxlim: 17399 bits: 16/15 c ---[ 435]---> Adder-cost: 250 maxlim: 15352 bits: 15/14 c ---[ 434]---> Adder-cost: 362 maxlim: 21493 bits: 16/15 c ---[ 433]---> Adder-cost: 381 maxlim: 23540 bits: 16/15 c ---[ 432]---> Adder-cost: 352 maxlim: 21493 bits: 16/15 c ---[ 431]---> Adder-cost: 428 maxlim: 23540 bits: 16/15 c ---[ 430]---> Adder-cost: 423 maxlim: 25587 bits: 16/15 c ---[ 429]---> Adder-cost: 300 maxlim: 25587 bits: 16/15 c ---[ 428]---> Adder-cost: 410 maxlim: 28657 bits: 16/15 c ---[ 427]---> Adder-cost: 465 maxlim: 31728 bits: 16/15 c ---[ 426]---> Adder-cost: 389 maxlim: 27634 bits: 16/15 c ---[ 425]---> Adder-cost: 354 maxlim: 27634 bits: 16/15 c ---[ 424]---> Adder-cost: 578 maxlim: 32751 bits: 16/15 c ---[ 423]---> Adder-cost: 604 maxlim: 35822 bits: 17/16 c ---[ 422]---> Adder-cost: 535 maxlim: 31728 bits: 16/15 c ---[ 421]---> Adder-cost: 577 maxlim: 38892 bits: 17/16 c ---[ 420]---> Adder-cost: 576 maxlim: 41963 bits: 17/16 c ---[ 419]---> Adder-cost: 670 maxlim: 35822 bits: 17/16 c ---[ 418]---> Adder-cost: 673 maxlim: 45033 bits: 17/16 c ---[ 417]---> Adder-cost: 644 maxlim: 48104 bits: 17/16 c ---[ 416]---> Adder-cost: 676 maxlim: 41963 bits: 17/16 c ---[ 415]---> Adder-cost: 757 maxlim: 47080 bits: 17/16 c ---[ 414]---> Adder-cost: 772 maxlim: 50151 bits: 17/16 c ---[ 413]---> Adder-cost: 838 maxlim: 44010 bits: 17/16 c ---[ 412]---> Adder-cost: 819 maxlim: 49127 bits: 17/16 c ---[ 411]---> Adder-cost: 820 maxlim: 52198 bits: 17/16 c ---[ 410]---> Adder-cost: 774 maxlim: 46057 bits: 17/16 c ---[ 409]---> BDD-cost: 36 c ---[ 408]---> Sorter-cost: 431 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 407]---> BDD-cost: 94 c ---[ 406]---> BDD-cost: 94 c ---[ 405]---> BDD-cost: 95 c ---[ 404]---> BDD-cost: 94 c ---[ 403]---> Sorter-cost: 673 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 402]---> Sorter-cost: 669 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 401]---> Sorter-cost: 1129 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 400]---> Sorter-cost: 1239 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 399]---> BDD-cost: 95 c ---[ 398]---> BDD-cost: 94 c ---[ 397]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 396]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 395]---> BDD-cost: 94 c ---[ 394]---> BDD-cost: 93 c ---[ 393]---> BDD-cost: 92 c ---[ 392]---> BDD-cost: 94 c ---[ 391]---> BDD-cost: 93 c ---[ 390]---> BDD-cost: 92 c ---[ 389]---> BDD-cost: 94 c ---[ 388]---> BDD-cost: 0 c ---[ 387]---> Sorter-cost: 651 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 386]---> Sorter-cost: 647 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 385]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 384]---> BDD-cost: 95 c ---[ 383]---> BDD-cost: 94 c ---[ 382]---> BDD-cost: 94 c ---[ 381]---> Sorter-cost: 671 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 380]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 379]---> Sorter-cost: 1390 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 378]---> Sorter-cost: 1482 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 377]---> Sorter-cost: 1013 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 376]---> BDD-cost: 94 c ---[ 374]---> Sorter-cost: 432 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 373]---> Sorter-cost: 669 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 372]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 371]---> Adder-cost: 227 maxlim: 10235 bits: 15/14 c ---[ 370]---> Adder-cost: 250 maxlim: 10234 bits: 15/14 c ---[ 369]---> Adder-cost: 251 maxlim: 14329 bits: 15/14 c ---[ 368]---> Adder-cost: 248 maxlim: 14328 bits: 15/14 c ---[ 367]---> Adder-cost: 317 maxlim: 16376 bits: 15/14 c ---[ 366]---> Adder-cost: 330 maxlim: 16375 bits: 15/14 c ---[ 365]---> Sorter-cost: 1215 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 364]---> Adder-cost: 312 maxlim: 18423 bits: 16/15 c ---[ 363]---> Adder-cost: 335 maxlim: 18422 bits: 16/15 c ---[ 362]---> Adder-cost: 560 maxlim: 18422 bits: 16/15 c ---[ 361]---> Adder-cost: 559 maxlim: 20469 bits: 16/15 c ---[ 360]---> Adder-cost: 418 maxlim: 20469 bits: 16/15 c ---[ 359]---> Adder-cost: 461 maxlim: 22516 bits: 16/15 c ---[ 358]---> BDD-cost: 92 c ---[ 357]---> BDD-cost: 94 c ---[ 355]---> BDD-cost: 50 c ---[ 353]---> BDD-cost: 50 c ---[ 351]---> BDD-cost: 50 c ---[ 349]---> BDD-cost: 50 c ---[ 347]---> BDD-cost: 50 c ---[ 345]---> BDD-cost: 50 c ---[ 343]---> BDD-cost: 50 c ---[ 341]---> BDD-cost: 50 c ---[ 339]---> BDD-cost: 50 c ---[ 337]---> BDD-cost: 50 c ---[ 335]---> BDD-cost: 50 c ---[ 333]---> BDD-cost: 50 c ---[ 331]---> BDD-cost: 50 c ---[ 329]---> BDD-cost: 50 c ---[ 327]---> BDD-cost: 50 c ---[ 325]---> BDD-cost: 50 c ---[ 323]---> BDD-cost: 50 c ---[ 321]---> BDD-cost: 50 c ---[ 319]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 317]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 315]---> BDD-cost: 50 c ---[ 313]---> BDD-cost: 50 c ---[ 311]---> BDD-cost: 50 c ---[ 309]---> BDD-cost: 50 c ---[ 307]---> BDD-cost: 50 c ---[ 305]---> BDD-cost: 50 c ---[ 303]---> BDD-cost: 50 c ---[ 301]---> BDD-cost: 50 c ---[ 299]---> BDD-cost: 50 c ---[ 297]---> BDD-cost: 50 c ---[ 295]---> BDD-cost: 50 c ---[ 293]---> BDD-cost: 50 c ---[ 291]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 289]---> BDD-cost: 50 c ---[ 287]---> BDD-cost: 50 c ---[ 285]---> BDD-cost: 50 c ---[ 283]---> BDD-cost: 50 c ---[ 281]---> BDD-cost: 50 c ---[ 279]---> BDD-cost: 50 c ---[ 277]---> BDD-cost: 50 c ---[ 275]---> BDD-cost: 50 c ---[ 273]---> BDD-cost: 50 c ---[ 271]---> BDD-cost: 50 c ---[ 269]---> BDD-cost: 50 c ---[ 267]---> BDD-cost: 50 c ---[ 265]---> BDD-cost: 50 c ---[ 263]---> BDD-cost: 50 c ---[ 261]---> BDD-cost: 50 c ---[ 259]---> BDD-cost: 50 c ---[ 257]---> BDD-cost: 50 c ---[ 255]---> BDD-cost: 50 c ---[ 253]---> BDD-cost: 50 c ---[ 251]---> BDD-cost: 50 c ---[ 249]---> BDD-cost: 50 c ---[ 247]---> BDD-cost: 50 c ---[ 245]---> BDD-cost: 50 c ---[ 243]---> BDD-cost: 50 c ---[ 241]---> BDD-cost: 50 c ---[ 239]---> BDD-cost: 50 c ---[ 237]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 235]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 233]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 231]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 229]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 227]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 225]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 223]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 221]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 219]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 217]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 213]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 211]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 209]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 207]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 205]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 203]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 201]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 197]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 195]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 193]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 191]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 189]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 187]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 185]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 181]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 179]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 177]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 175]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 173]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 167]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 165]---> BDD-cost: 50 c ---[ 163]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 161]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 159]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 157]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 155]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 153]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 151]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 149]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 147]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 145]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 143]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 141]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 139]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 137]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 135]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 133]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 131]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 129]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 127]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 125]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 123]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 121]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 117]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 115]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> BDD-cost: 50 c ---[ 109]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 97]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 95]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 93]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 91]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 89]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 87]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 85]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 83]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 81]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 79]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 77]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 75]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 73]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 71]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 67]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 37]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> BDD-cost: 50 c ---[ 29]---> BDD-cost: 50 c ---[ 27]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 19]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 17]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 15]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 13]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 3]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> BDD-cost: 29 c ---[ 1]---> BDD-cost: 28 c ---[ 0]---> BDD-cost: 32 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 725889 2144458 | 241963 0 0 nan | 0.000 % | c | 100 | 725889 2144458 | 266159 100 2354 23.5 | 7.276 % | c | 250 | 725880 2144439 | 292775 248 3029 12.2 | 7.277 % | c | 475 | 725880 2144439 | 322052 473 4119 8.7 | 7.277 % | c | 813 | 725871 2144420 | 354258 810 5934 7.3 | 7.279 % | c | 1319 | 725816 2144298 | 389683 1308 8401 6.4 | 7.287 % | c | 2078 | 725785 2144230 | 428652 2064 11809 5.7 | 7.291 % | c | 3217 | 725422 2143413 | 471517 3150 16439 5.2 | 7.341 % | c | 4925 | 725206 2142931 | 518669 4832 25552 5.3 | 7.371 % | c | 7487 | 724760 2141935 | 570536 7324 38468 5.3 | 7.433 % | c | 11331 | 724593 2141562 | 627589 11145 59648 5.4 | 7.456 % | c | 17098 | 724045 2140320 | 690348 16819 106259 6.3 | 7.532 % | c | 25747 | 723671 2139469 | 759383 25416 191105 7.5 | 7.583 % | c | 38721 | 722944 2137790 | 835321 38285 313771 8.2 | 7.683 % | c | 58184 | 722826 2137519 | 918854 57731 953217 16.5 | 7.699 % | c | 87379 | 722438 2136582 | 1010739 86877 1820020 20.9 | 7.750 % | c | 131168 | 721981 2135503 | 1111813 130596 2941205 22.5 | 7.811 % | c | 196855 | 721916 2135349 | 1222994 196270 5363973 27.3 | 7.820 % | c | 295381 | 721565 2134485 | 1345294 294736 7998638 27.1 | 7.866 % |
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/12206/stat): 12206 (minisat+_script) R 12205 12206 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785819968 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/12206/statm): 174 3 169 147 0 27 0 [pid=12206] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=12207 New process pid=12208 New process pid=12209 execve syscall for /bin/sed executable One traced child (pid=12208) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=12209) exited with status: 0 One traced child (pid=12207) exited with status: 0 New process pid=12210 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-degen2.opb [startup+10.0037 s] Raw data (loadavg): 0.93 0.98 0.97 1/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) T 12206 12206 31778 0 -1 0 9819 0 0 0 914 41 0 0 23 0 1 0 1785819973 41701376 9057 4294967295 134512640 135094434 3221224432 3221209580 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/12210/statm): 10181 9057 145 145 0 10036 0 [pid=12210] vsize: 40724 Current children cumulated CPU time (s) 9.55 Current children cumulated vsize (Kb) 42848 [startup+20.0056 s] Raw data (loadavg): 0.94 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18148 0 0 0 1834 81 0 0 25 0 1 0 1785819973 77860864 17386 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19009 17386 145 145 0 18864 0 [pid=12210] vsize: 76036 Current children cumulated CPU time (s) 19.15 Current children cumulated vsize (Kb) 78160 [startup+30.0074 s] Raw data (loadavg): 0.95 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18188 0 0 0 2832 82 0 0 25 0 1 0 1785819973 78024704 17426 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19049 17426 145 145 0 18904 0 [pid=12210] vsize: 76196 Current children cumulated CPU time (s) 29.14 Current children cumulated vsize (Kb) 78320 [startup+40.0082 s] Raw data (loadavg): 0.96 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18285 0 0 0 3831 82 0 0 25 0 1 0 1785819973 78430208 17523 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 19148 17523 145 145 0 19003 0 [pid=12210] vsize: 76592 Current children cumulated CPU time (s) 39.13 Current children cumulated vsize (Kb) 78716 [startup+50.01 s] Raw data (loadavg): 0.96 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18326 0 0 0 4831 82 0 0 25 0 1 0 1785819973 78622720 17564 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 19195 17564 145 145 0 19050 0 [pid=12210] vsize: 76780 Current children cumulated CPU time (s) 49.13 Current children cumulated vsize (Kb) 78904 [startup+60.0108 s] Raw data (loadavg): 0.97 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18379 0 0 0 5830 82 0 0 25 0 1 0 1785819973 78827520 17617 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 19245 17617 145 145 0 19100 0 [pid=12210] vsize: 76980 Current children cumulated CPU time (s) 59.12 Current children cumulated vsize (Kb) 79104 [startup+70.0127 s] Raw data (loadavg): 0.97 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18423 0 0 0 6829 83 0 0 23 0 1 0 1785819973 78999552 17661 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19287 17661 145 145 0 19142 0 [pid=12210] vsize: 77148 Current children cumulated CPU time (s) 69.12 Current children cumulated vsize (Kb) 79272 [startup+80.0145 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18447 0 0 0 7828 83 0 0 25 0 1 0 1785819973 79089664 17685 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19309 17685 145 145 0 19164 0 [pid=12210] vsize: 77236 Current children cumulated CPU time (s) 79.11 Current children cumulated vsize (Kb) 79360 [startup+90.0153 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18488 0 0 0 8827 84 0 0 25 0 1 0 1785819973 79314944 17726 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19364 17726 145 145 0 19219 0 [pid=12210] vsize: 77456 Current children cumulated CPU time (s) 89.11 Current children cumulated vsize (Kb) 79580 [startup+100.017 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18513 0 0 0 9827 85 0 0 25 0 1 0 1785819973 79409152 17751 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19387 17751 145 145 0 19242 0 [pid=12210] vsize: 77548 Current children cumulated CPU time (s) 99.12 Current children cumulated vsize (Kb) 79672 [startup+110.019 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18603 0 0 0 10825 86 0 0 25 0 1 0 1785819973 79753216 17841 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19471 17841 145 145 0 19326 0 [pid=12210] vsize: 77884 Current children cumulated CPU time (s) 109.11 Current children cumulated vsize (Kb) 80008 [startup+120.021 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18653 0 0 0 11824 86 0 0 25 0 1 0 1785819973 79929344 17891 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19514 17891 145 145 0 19369 0 [pid=12210] vsize: 78056 Current children cumulated CPU time (s) 119.1 Current children cumulated vsize (Kb) 80180 [startup+130.022 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18728 0 0 0 12822 87 0 0 25 0 1 0 1785819973 80216064 17966 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19584 17966 145 145 0 19439 0 [pid=12210] vsize: 78336 Current children cumulated CPU time (s) 129.09 Current children cumulated vsize (Kb) 80460 [startup+140.022 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18763 0 0 0 13821 88 0 0 25 0 1 0 1785819973 80351232 18001 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19617 18001 145 145 0 19472 0 [pid=12210] vsize: 78468 Current children cumulated CPU time (s) 139.09 Current children cumulated vsize (Kb) 80592 [startup+150.024 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18833 0 0 0 14820 89 0 0 25 0 1 0 1785819973 80756736 18071 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19716 18071 145 145 0 19571 0 [pid=12210] vsize: 78864 Current children cumulated CPU time (s) 149.09 Current children cumulated vsize (Kb) 80988 [startup+160.025 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18856 0 0 0 15819 90 0 0 25 0 1 0 1785819973 80842752 18094 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19737 18094 145 145 0 19592 0 [pid=12210] vsize: 78948 Current children cumulated CPU time (s) 159.09 Current children cumulated vsize (Kb) 81072 [startup+170.027 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18954 0 0 0 16817 91 0 0 25 0 1 0 1785819973 81227776 18192 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19831 18192 145 145 0 19686 0 [pid=12210] vsize: 79324 Current children cumulated CPU time (s) 169.08 Current children cumulated vsize (Kb) 81448 [startup+180.028 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 19072 0 0 0 17815 92 0 0 25 0 1 0 1785819973 81674240 18310 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 19940 18310 145 145 0 19795 0 [pid=12210] vsize: 79760 Current children cumulated CPU time (s) 179.07 Current children cumulated vsize (Kb) 81884 [startup+190.028 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 19324 0 0 0 18809 95 0 0 25 0 1 0 1785819973 82677760 18562 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 20185 18562 145 145 0 20040 0 [pid=12210] vsize: 80740 Current children cumulated CPU time (s) 189.04 Current children cumulated vsize (Kb) 82864 [startup+200.032 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 19800 0 0 0 19801 99 0 0 25 0 1 0 1785819973 84598784 19038 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 20654 19038 145 145 0 20509 0 [pid=12210] vsize: 82616 Current children cumulated CPU time (s) 199 Current children cumulated vsize (Kb) 84740 [startup+210.033 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20153 0 0 0 20796 101 0 0 25 0 1 0 1785819973 86274048 19391 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 21063 19391 145 145 0 20918 0 [pid=12210] vsize: 84252 Current children cumulated CPU time (s) 208.97 Current children cumulated vsize (Kb) 86376 [startup+220.035 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20199 0 0 0 21796 101 0 0 25 0 1 0 1785819973 86454272 19437 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 21107 19437 145 145 0 20962 0 [pid=12210] vsize: 84428 Current children cumulated CPU time (s) 218.97 Current children cumulated vsize (Kb) 86552 [startup+230.036 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20229 0 0 0 22795 101 0 0 25 0 1 0 1785819973 86573056 19467 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 21136 19467 145 145 0 20991 0 [pid=12210] vsize: 84544 Current children cumulated CPU time (s) 228.96 Current children cumulated vsize (Kb) 86668 [startup+240.037 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20281 0 0 0 23795 102 0 0 25 0 1 0 1785819973 86777856 19519 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 21186 19519 145 145 0 21041 0 [pid=12210] vsize: 84744 Current children cumulated CPU time (s) 238.97 Current children cumulated vsize (Kb) 86868 [startup+250.037 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20347 0 0 0 24793 102 0 0 25 0 1 0 1785819973 87019520 19585 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 21245 19585 145 145 0 21100 0 [pid=12210] vsize: 84980 Current children cumulated CPU time (s) 248.95 Current children cumulated vsize (Kb) 87104 [startup+260.038 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20883 0 0 0 25786 105 0 0 25 0 1 0 1785819973 89174016 20121 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 21771 20121 145 145 0 21626 0 [pid=12210] vsize: 87084 Current children cumulated CPU time (s) 258.91 Current children cumulated vsize (Kb) 89208 [startup+270.039 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21055 0 0 0 26783 106 0 0 25 0 1 0 1785819973 89870336 20293 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 21941 20293 145 145 0 21796 0 [pid=12210] vsize: 87764 Current children cumulated CPU time (s) 268.89 Current children cumulated vsize (Kb) 89888 [startup+280.04 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21099 0 0 0 27782 107 0 0 25 0 1 0 1785819973 90042368 20337 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 21983 20337 145 145 0 21838 0 [pid=12210] vsize: 87932 Current children cumulated CPU time (s) 278.89 Current children cumulated vsize (Kb) 90056 [startup+290.041 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21135 0 0 0 28782 107 0 0 25 0 1 0 1785819973 90181632 20373 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 22017 20373 145 145 0 21872 0 [pid=12210] vsize: 88068 Current children cumulated CPU time (s) 288.89 Current children cumulated vsize (Kb) 90192 [startup+300.041 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21185 0 0 0 29781 107 0 0 25 0 1 0 1785819973 90382336 20423 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 22066 20423 145 145 0 21921 0 [pid=12210] vsize: 88264 Current children cumulated CPU time (s) 298.88 Current children cumulated vsize (Kb) 90388 [startup+310.042 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21214 0 0 0 30781 107 0 0 25 0 1 0 1785819973 90492928 20452 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 22093 20452 145 145 0 21948 0 [pid=12210] vsize: 88372 Current children cumulated CPU time (s) 308.88 Current children cumulated vsize (Kb) 90496 [startup+320.043 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21322 0 0 0 31780 108 0 0 25 0 1 0 1785819973 90918912 20560 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 22197 20560 145 145 0 22052 0 [pid=12210] vsize: 88788 Current children cumulated CPU time (s) 318.88 Current children cumulated vsize (Kb) 90912 [startup+330.044 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21989 0 0 0 32768 113 0 0 25 0 1 0 1785819973 93605888 21227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 22853 21227 145 145 0 22708 0 [pid=12210] vsize: 91412 Current children cumulated CPU time (s) 328.81 Current children cumulated vsize (Kb) 93536 [startup+340.045 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 22270 0 0 0 33763 115 0 0 25 0 1 0 1785819973 94728192 21508 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 23127 21508 145 145 0 22982 0 [pid=12210] vsize: 92508 Current children cumulated CPU time (s) 338.78 Current children cumulated vsize (Kb) 94632 [startup+350.047 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 22335 0 0 0 34763 115 0 0 25 0 1 0 1785819973 94982144 21573 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 23189 21573 145 145 0 23044 0 [pid=12210] vsize: 92756 Current children cumulated CPU time (s) 348.78 Current children cumulated vsize (Kb) 94880 [startup+360.047 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 22459 0 0 0 35760 116 0 0 25 0 1 0 1785819973 95473664 21697 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 23309 21697 145 145 0 23164 0 [pid=12210] vsize: 93236 Current children cumulated CPU time (s) 358.76 Current children cumulated vsize (Kb) 95360 [startup+370.048 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 22755 0 0 0 36757 117 0 0 25 0 1 0 1785819973 97185792 21993 4294967295 134512640 135094434 3221224432 3221223104 134556523 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 23727 21993 145 145 0 23582 0 [pid=12210] vsize: 94908 Current children cumulated CPU time (s) 368.74 Current children cumulated vsize (Kb) 97032 [startup+380.049 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 23283 0 0 0 37746 123 0 0 25 0 1 0 1785819973 99315712 22521 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 24247 22521 145 145 0 24102 0 [pid=12210] vsize: 96988 Current children cumulated CPU time (s) 378.69 Current children cumulated vsize (Kb) 99112 [startup+390.05 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 23667 0 0 0 38741 126 0 0 25 0 1 0 1785819973 100872192 22905 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 24627 22905 145 145 0 24482 0 [pid=12210] vsize: 98508 Current children cumulated CPU time (s) 388.67 Current children cumulated vsize (Kb) 100632 [startup+400.051 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 23998 0 0 0 39736 128 0 0 25 0 1 0 1785819973 102203392 23236 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 24952 23236 145 145 0 24807 0 [pid=12210] vsize: 99808 Current children cumulated CPU time (s) 398.64 Current children cumulated vsize (Kb) 101932 [startup+410.052 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 24297 0 0 0 40731 130 0 0 25 0 1 0 1785819973 103428096 23535 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 25251 23535 145 145 0 25106 0 [pid=12210] vsize: 101004 Current children cumulated CPU time (s) 408.61 Current children cumulated vsize (Kb) 103128 [startup+420.053 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 24572 0 0 0 41726 133 0 0 25 0 1 0 1785819973 104542208 23810 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 25523 23810 145 145 0 25378 0 [pid=12210] vsize: 102092 Current children cumulated CPU time (s) 418.59 Current children cumulated vsize (Kb) 104216 [startup+430.054 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 24767 0 0 0 42722 135 0 0 25 0 1 0 1785819973 105320448 24005 4294967295 134512640 135094434 3221224432 3221223044 134563085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 25713 24005 145 145 0 25568 0 [pid=12210] vsize: 102852 Current children cumulated CPU time (s) 428.57 Current children cumulated vsize (Kb) 104976 [startup+440.055 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 24834 0 0 0 43721 136 0 0 25 0 1 0 1785819973 105615360 24072 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 25785 24072 145 145 0 25640 0 [pid=12210] vsize: 103140 Current children cumulated CPU time (s) 438.57 Current children cumulated vsize (Kb) 105264 [startup+450.057 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25014 0 0 0 44718 137 0 0 25 0 1 0 1785819973 106340352 24252 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 25962 24252 145 145 0 25817 0 [pid=12210] vsize: 103848 Current children cumulated CPU time (s) 448.55 Current children cumulated vsize (Kb) 105972 [startup+460.058 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25108 0 0 0 45716 137 0 0 25 0 1 0 1785819973 106717184 24346 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 26054 24346 145 145 0 25909 0 [pid=12210] vsize: 104216 Current children cumulated CPU time (s) 458.53 Current children cumulated vsize (Kb) 106340 [startup+470.058 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25333 0 0 0 46712 139 0 0 25 0 1 0 1785819973 107622400 24571 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 26275 24571 145 145 0 26130 0 [pid=12210] vsize: 105100 Current children cumulated CPU time (s) 468.51 Current children cumulated vsize (Kb) 107224 [startup+480.06 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25730 0 0 0 47706 141 0 0 25 0 1 0 1785819973 109199360 24968 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 26660 24968 145 145 0 26515 0 [pid=12210] vsize: 106640 Current children cumulated CPU time (s) 478.47 Current children cumulated vsize (Kb) 108764 [startup+490.061 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25864 0 0 0 48702 143 0 0 25 0 1 0 1785819973 109731840 25102 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 26790 25102 145 145 0 26645 0 [pid=12210] vsize: 107160 Current children cumulated CPU time (s) 488.45 Current children cumulated vsize (Kb) 109284 [startup+500.062 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25961 0 0 0 49701 143 0 0 25 0 1 0 1785819973 110116864 25199 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 26884 25199 145 145 0 26739 0 [pid=12210] vsize: 107536 Current children cumulated CPU time (s) 498.44 Current children cumulated vsize (Kb) 109660 [startup+510.063 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26110 0 0 0 50698 145 0 0 25 0 1 0 1785819973 110710784 25348 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27029 25348 145 145 0 26884 0 [pid=12210] vsize: 108116 Current children cumulated CPU time (s) 508.43 Current children cumulated vsize (Kb) 110240 [startup+520.064 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26253 0 0 0 51695 147 0 0 25 0 1 0 1785819973 111280128 25491 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27168 25491 145 145 0 27023 0 [pid=12210] vsize: 108672 Current children cumulated CPU time (s) 518.42 Current children cumulated vsize (Kb) 110796 [startup+530.064 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26329 0 0 0 52694 148 0 0 25 0 1 0 1785819973 111583232 25567 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27242 25567 145 145 0 27097 0 [pid=12210] vsize: 108968 Current children cumulated CPU time (s) 528.42 Current children cumulated vsize (Kb) 111092 [startup+540.065 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26450 0 0 0 53692 149 0 0 25 0 1 0 1785819973 112054272 25688 4294967295 134512640 135094434 3221224432 3221223044 134563115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27357 25688 145 145 0 27212 0 [pid=12210] vsize: 109428 Current children cumulated CPU time (s) 538.41 Current children cumulated vsize (Kb) 111552 [startup+550.067 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26494 0 0 0 54691 149 0 0 25 0 1 0 1785819973 112242688 25732 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27403 25732 145 145 0 27258 0 [pid=12210] vsize: 109612 Current children cumulated CPU time (s) 548.4 Current children cumulated vsize (Kb) 111736 [startup+560.068 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26631 0 0 0 55689 150 0 0 25 0 1 0 1785819973 112771072 25869 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27532 25869 145 145 0 27387 0 [pid=12210] vsize: 110128 Current children cumulated CPU time (s) 558.39 Current children cumulated vsize (Kb) 112252 [startup+570.069 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26696 0 0 0 56688 151 0 0 25 0 1 0 1785819973 113029120 25934 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27595 25934 145 145 0 27450 0 [pid=12210] vsize: 110380 Current children cumulated CPU time (s) 568.39 Current children cumulated vsize (Kb) 112504 [startup+580.069 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26746 0 0 0 57688 151 0 0 25 0 1 0 1785819973 113221632 25984 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27642 25984 145 145 0 27497 0 [pid=12210] vsize: 110568 Current children cumulated CPU time (s) 578.39 Current children cumulated vsize (Kb) 112692 [startup+590.07 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26794 0 0 0 58687 152 0 0 25 0 1 0 1785819973 113410048 26032 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27688 26032 145 145 0 27543 0 [pid=12210] vsize: 110752 Current children cumulated CPU time (s) 588.39 Current children cumulated vsize (Kb) 112876 [startup+600.072 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26831 0 0 0 59687 152 0 0 25 0 1 0 1785819973 113553408 26069 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27723 26069 145 145 0 27578 0 [pid=12210] vsize: 110892 Current children cumulated CPU time (s) 598.39 Current children cumulated vsize (Kb) 113016 [startup+610.073 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26859 0 0 0 60687 152 0 0 25 0 1 0 1785819973 113664000 26097 4294967295 134512640 135094434 3221224432 3221223072 134562131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27750 26097 145 145 0 27605 0 [pid=12210] vsize: 111000 Current children cumulated CPU time (s) 608.39 Current children cumulated vsize (Kb) 113124 [startup+620.075 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26907 0 0 0 61686 152 0 0 25 0 1 0 1785819973 113852416 26145 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27796 26145 145 145 0 27651 0 [pid=12210] vsize: 111184 Current children cumulated CPU time (s) 618.38 Current children cumulated vsize (Kb) 113308 [startup+630.076 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26945 0 0 0 62686 153 0 0 25 0 1 0 1785819973 113995776 26183 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27831 26183 145 145 0 27686 0 [pid=12210] vsize: 111324 Current children cumulated CPU time (s) 628.39 Current children cumulated vsize (Kb) 113448 [startup+640.076 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26984 0 0 0 63685 153 0 0 25 0 1 0 1785819973 114122752 26222 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27862 26222 145 145 0 27717 0 [pid=12210] vsize: 111448 Current children cumulated CPU time (s) 638.38 Current children cumulated vsize (Kb) 113572 [startup+650.078 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27017 0 0 0 64684 154 0 0 25 0 1 0 1785819973 114249728 26255 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27893 26255 145 145 0 27748 0 [pid=12210] vsize: 111572 Current children cumulated CPU time (s) 648.38 Current children cumulated vsize (Kb) 113696 [startup+660.079 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27051 0 0 0 65683 154 0 0 25 0 1 0 1785819973 114384896 26289 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27926 26289 145 145 0 27781 0 [pid=12210] vsize: 111704 Current children cumulated CPU time (s) 658.37 Current children cumulated vsize (Kb) 113828 [startup+670.08 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27094 0 0 0 66683 155 0 0 25 0 1 0 1785819973 114556928 26332 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 27968 26332 145 145 0 27823 0 [pid=12210] vsize: 111872 Current children cumulated CPU time (s) 668.38 Current children cumulated vsize (Kb) 113996 [startup+680.081 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27162 0 0 0 67682 155 0 0 25 0 1 0 1785819973 114827264 26400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28034 26400 145 145 0 27889 0 [pid=12210] vsize: 112136 Current children cumulated CPU time (s) 678.37 Current children cumulated vsize (Kb) 114260 [startup+690.082 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27241 0 0 0 68681 156 0 0 25 0 1 0 1785819973 115138560 26479 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28110 26479 145 145 0 27965 0 [pid=12210] vsize: 112440 Current children cumulated CPU time (s) 688.37 Current children cumulated vsize (Kb) 114564 [startup+700.082 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27284 0 0 0 69680 156 0 0 25 0 1 0 1785819973 115306496 26522 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28151 26522 145 145 0 28006 0 [pid=12210] vsize: 112604 Current children cumulated CPU time (s) 698.36 Current children cumulated vsize (Kb) 114728 [startup+710.083 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27372 0 0 0 70679 156 0 0 25 0 1 0 1785819973 115662848 26610 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28238 26610 145 145 0 28093 0 [pid=12210] vsize: 112952 Current children cumulated CPU time (s) 708.35 Current children cumulated vsize (Kb) 115076 [startup+720.085 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27420 0 0 0 71679 157 0 0 25 0 1 0 1785819973 115855360 26658 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28285 26658 145 145 0 28140 0 [pid=12210] vsize: 113140 Current children cumulated CPU time (s) 718.36 Current children cumulated vsize (Kb) 115264 [startup+730.086 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27465 0 0 0 72678 157 0 0 25 0 1 0 1785819973 116031488 26703 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28328 26703 145 145 0 28183 0 [pid=12210] vsize: 113312 Current children cumulated CPU time (s) 728.35 Current children cumulated vsize (Kb) 115436 [startup+740.087 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27501 0 0 0 73677 157 0 0 25 0 1 0 1785819973 116170752 26739 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28362 26739 145 145 0 28217 0 [pid=12210] vsize: 113448 Current children cumulated CPU time (s) 738.34 Current children cumulated vsize (Kb) 115572 [startup+750.088 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27586 0 0 0 74675 158 0 0 25 0 1 0 1785819973 116510720 26824 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28445 26824 145 145 0 28300 0 [pid=12210] vsize: 113780 Current children cumulated CPU time (s) 748.33 Current children cumulated vsize (Kb) 115904 [startup+760.089 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27648 0 0 0 75675 158 0 0 25 0 1 0 1785819973 117800960 26886 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28760 26886 145 145 0 28615 0 [pid=12210] vsize: 115040 Current children cumulated CPU time (s) 758.33 Current children cumulated vsize (Kb) 117164 [startup+770.09 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27713 0 0 0 76674 159 0 0 25 0 1 0 1785819973 118071296 26951 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28826 26951 145 145 0 28681 0 [pid=12210] vsize: 115304 Current children cumulated CPU time (s) 768.33 Current children cumulated vsize (Kb) 117428 [startup+780.092 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27765 0 0 0 77673 160 0 0 25 0 1 0 1785819973 118276096 27003 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 28876 27003 145 145 0 28731 0 [pid=12210] vsize: 115504 Current children cumulated CPU time (s) 778.33 Current children cumulated vsize (Kb) 117628 [startup+790.093 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27906 0 0 0 78671 160 0 0 25 0 1 0 1785819973 118837248 27144 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 29013 27144 145 145 0 28868 0 [pid=12210] vsize: 116052 Current children cumulated CPU time (s) 788.31 Current children cumulated vsize (Kb) 118176 [startup+800.094 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27985 0 0 0 79670 161 0 0 25 0 1 0 1785819973 119152640 27223 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 29090 27223 145 145 0 28945 0 [pid=12210] vsize: 116360 Current children cumulated CPU time (s) 798.31 Current children cumulated vsize (Kb) 118484 [startup+810.094 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 28033 0 0 0 80670 162 0 0 25 0 1 0 1785819973 119341056 27271 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 29136 27271 145 145 0 28991 0 [pid=12210] vsize: 116544 Current children cumulated CPU time (s) 808.32 Current children cumulated vsize (Kb) 118668 [startup+820.096 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 28735 0 0 0 81656 167 0 0 25 0 1 0 1785819973 122195968 27973 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 29833 27973 145 145 0 29688 0 [pid=12210] vsize: 119332 Current children cumulated CPU time (s) 818.23 Current children cumulated vsize (Kb) 121456 [startup+830.097 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 28980 0 0 0 82653 169 0 0 25 0 1 0 1785819973 123183104 28218 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 30074 28218 145 145 0 29929 0 [pid=12210] vsize: 120296 Current children cumulated CPU time (s) 828.22 Current children cumulated vsize (Kb) 122420 [startup+840.098 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 29349 0 0 0 83646 172 0 0 25 0 1 0 1785819973 124674048 28587 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 30438 28587 145 145 0 30293 0 [pid=12210] vsize: 121752 Current children cumulated CPU time (s) 838.18 Current children cumulated vsize (Kb) 123876 [startup+850.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 29395 0 0 0 84646 172 0 0 25 0 1 0 1785819973 124854272 28633 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 30482 28633 145 145 0 30337 0 [pid=12210] vsize: 121928 Current children cumulated CPU time (s) 848.18 Current children cumulated vsize (Kb) 124052 [startup+860.101 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 29503 0 0 0 85644 173 0 0 25 0 1 0 1785819973 125284352 28741 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 30587 28741 145 145 0 30442 0 [pid=12210] vsize: 122348 Current children cumulated CPU time (s) 858.17 Current children cumulated vsize (Kb) 124472 [startup+870.102 s] Raw data (loadavg): 0.99 0.98 0.97 1/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) T 12206 12206 31778 0 -1 0 29636 0 0 0 86641 173 0 0 25 0 1 0 1785819973 125816832 28874 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/12210/statm): 30717 28874 145 145 0 30572 0 [pid=12210] vsize: 122868 Current children cumulated CPU time (s) 868.14 Current children cumulated vsize (Kb) 124992 [startup+880.104 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30058 0 0 0 87633 177 0 0 25 0 1 0 1785819973 127520768 29296 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 31133 29296 145 145 0 30988 0 [pid=12210] vsize: 124532 Current children cumulated CPU time (s) 878.1 Current children cumulated vsize (Kb) 126656 [startup+890.105 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30468 0 0 0 88625 179 0 0 25 0 1 0 1785819973 129183744 29706 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 31539 29706 145 145 0 31394 0 [pid=12210] vsize: 126156 Current children cumulated CPU time (s) 888.04 Current children cumulated vsize (Kb) 128280 [startup+900.107 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30661 0 0 0 89621 180 0 0 25 0 1 0 1785819973 129978368 29899 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 31733 29899 145 145 0 31588 0 [pid=12210] vsize: 126932 Current children cumulated CPU time (s) 898.01 Current children cumulated vsize (Kb) 129056 [startup+910.108 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30774 0 0 0 90619 182 0 0 25 0 1 0 1785819973 130433024 30012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 31844 30012 145 145 0 31699 0 [pid=12210] vsize: 127376 Current children cumulated CPU time (s) 908.01 Current children cumulated vsize (Kb) 129500 [startup+920.108 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30910 0 0 0 91616 182 0 0 25 0 1 0 1785819973 130977792 30148 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 31977 30148 145 145 0 31832 0 [pid=12210] vsize: 127908 Current children cumulated CPU time (s) 917.98 Current children cumulated vsize (Kb) 130032 [startup+930.109 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30973 0 0 0 92615 183 0 0 25 0 1 0 1785819973 131223552 30211 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32037 30211 145 145 0 31892 0 [pid=12210] vsize: 128148 Current children cumulated CPU time (s) 927.98 Current children cumulated vsize (Kb) 130272 [startup+940.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31064 0 0 0 93614 184 0 0 25 0 1 0 1785819973 131584000 30302 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32125 30302 145 145 0 31980 0 [pid=12210] vsize: 128500 Current children cumulated CPU time (s) 937.98 Current children cumulated vsize (Kb) 130624 [startup+950.112 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31115 0 0 0 94613 184 0 0 25 0 1 0 1785819973 131784704 30353 4294967295 134512640 135094434 3221224432 3221222976 134562149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32174 30353 145 145 0 32029 0 [pid=12210] vsize: 128696 Current children cumulated CPU time (s) 947.97 Current children cumulated vsize (Kb) 130820 [startup+960.113 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31170 0 0 0 95612 185 0 0 25 0 1 0 1785819973 131969024 30408 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32219 30408 145 145 0 32074 0 [pid=12210] vsize: 128876 Current children cumulated CPU time (s) 957.97 Current children cumulated vsize (Kb) 131000 [startup+970.114 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31244 0 0 0 96611 185 0 0 25 0 1 0 1785819973 132259840 30482 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32290 30482 145 145 0 32145 0 [pid=12210] vsize: 129160 Current children cumulated CPU time (s) 967.96 Current children cumulated vsize (Kb) 131284 [startup+980.114 s] Raw data (loadavg): 0.99 0.98 0.97 3/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31299 0 0 0 97610 186 0 0 25 0 1 0 1785819973 132476928 30537 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32343 30537 145 145 0 32198 0 [pid=12210] vsize: 129372 Current children cumulated CPU time (s) 977.96 Current children cumulated vsize (Kb) 131496 [startup+990.115 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31374 0 0 0 98609 186 0 0 25 0 1 0 1785819973 132775936 30612 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32416 30612 145 145 0 32271 0 [pid=12210] vsize: 129664 Current children cumulated CPU time (s) 987.95 Current children cumulated vsize (Kb) 131788 [startup+1000.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31417 0 0 0 99609 186 0 0 25 0 1 0 1785819973 132943872 30655 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32457 30655 145 145 0 32312 0 [pid=12210] vsize: 129828 Current children cumulated CPU time (s) 997.95 Current children cumulated vsize (Kb) 131952 [startup+1010.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31457 0 0 0 100608 187 0 0 25 0 1 0 1785819973 133103616 30695 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32496 30695 145 145 0 32351 0 [pid=12210] vsize: 129984 Current children cumulated CPU time (s) 1007.95 Current children cumulated vsize (Kb) 132108 [startup+1020.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31489 0 0 0 101608 187 0 0 25 0 1 0 1785819973 133226496 30727 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32526 30727 145 145 0 32381 0 [pid=12210] vsize: 130104 Current children cumulated CPU time (s) 1017.95 Current children cumulated vsize (Kb) 132228 [startup+1030.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31567 0 0 0 102606 188 0 0 25 0 1 0 1785819973 133537792 30805 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32602 30805 145 145 0 32457 0 [pid=12210] vsize: 130408 Current children cumulated CPU time (s) 1027.94 Current children cumulated vsize (Kb) 132532 [startup+1040.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31620 0 0 0 103605 188 0 0 25 0 1 0 1785819973 133746688 30858 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 32653 30858 145 145 0 32508 0 [pid=12210] vsize: 130612 Current children cumulated CPU time (s) 1037.93 Current children cumulated vsize (Kb) 132736 [startup+1050.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32084 0 0 0 104597 192 0 0 25 0 1 0 1785819973 135606272 31322 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 33107 31322 145 145 0 32962 0 [pid=12210] vsize: 132428 Current children cumulated CPU time (s) 1047.89 Current children cumulated vsize (Kb) 134552 [startup+1060.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32352 0 0 0 105593 193 0 0 25 0 1 0 1785819973 136671232 31590 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 33367 31590 145 145 0 33222 0 [pid=12210] vsize: 133468 Current children cumulated CPU time (s) 1057.86 Current children cumulated vsize (Kb) 135592 [startup+1070.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32465 0 0 0 106590 194 0 0 25 0 1 0 1785819973 137117696 31703 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 33476 31703 145 145 0 33331 0 [pid=12210] vsize: 133904 Current children cumulated CPU time (s) 1067.84 Current children cumulated vsize (Kb) 136028 [startup+1080.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32509 0 0 0 107590 195 0 0 25 0 1 0 1785819973 137293824 31747 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12210/statm): 33519 31747 145 145 0 33374 0 [pid=12210] vsize: 134076 Current children cumulated CPU time (s) 1077.85 Current children cumulated vsize (Kb) 136200 [startup+1090.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32638 0 0 0 108587 196 0 0 25 0 1 0 1785819973 137809920 31876 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 33645 31876 145 145 0 33500 0 [pid=12210] vsize: 134580 Current children cumulated CPU time (s) 1087.83 Current children cumulated vsize (Kb) 136704 [startup+1100.13 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32903 0 0 0 109583 198 0 0 25 0 1 0 1785819973 138883072 32141 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 33907 32141 145 145 0 33762 0 [pid=12210] vsize: 135628 Current children cumulated CPU time (s) 1097.81 Current children cumulated vsize (Kb) 137752 [startup+1110.13 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 33284 0 0 0 110576 201 0 0 25 0 1 0 1785819973 140427264 32522 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 34284 32522 145 145 0 34139 0 [pid=12210] vsize: 137136 Current children cumulated CPU time (s) 1107.77 Current children cumulated vsize (Kb) 139260 [startup+1120.13 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 33643 0 0 0 111569 204 0 0 25 0 1 0 1785819973 141885440 32881 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 34640 32881 145 145 0 34495 0 [pid=12210] vsize: 138560 Current children cumulated CPU time (s) 1117.73 Current children cumulated vsize (Kb) 140684 [startup+1130.13 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34004 0 0 0 112563 207 0 0 25 0 1 0 1785819973 143360000 33242 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 35000 33242 145 145 0 34855 0 [pid=12210] vsize: 140000 Current children cumulated CPU time (s) 1127.7 Current children cumulated vsize (Kb) 142124 [startup+1140.13 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34163 0 0 0 113559 208 0 0 25 0 1 0 1785819973 143990784 33401 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 35154 33401 145 145 0 35009 0 [pid=12210] vsize: 140616 Current children cumulated CPU time (s) 1137.67 Current children cumulated vsize (Kb) 142740 [startup+1150.13 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34541 0 0 0 114551 212 0 0 25 0 1 0 1785819973 145522688 33779 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 35528 33779 145 145 0 35383 0 [pid=12210] vsize: 142112 Current children cumulated CPU time (s) 1147.63 Current children cumulated vsize (Kb) 144236 [startup+1160.13 s] Raw data (loadavg): 1.06 1.00 0.98 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34796 0 0 0 115546 213 0 0 25 0 1 0 1785819973 146554880 34034 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 35780 34034 145 145 0 35635 0 [pid=12210] vsize: 143120 Current children cumulated CPU time (s) 1157.59 Current children cumulated vsize (Kb) 145244 [startup+1170.13 s] Raw data (loadavg): 1.05 1.00 0.98 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34858 0 0 0 116544 214 0 0 25 0 1 0 1785819973 146800640 34096 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 35840 34096 145 145 0 35695 0 [pid=12210] vsize: 143360 Current children cumulated CPU time (s) 1167.58 Current children cumulated vsize (Kb) 145484 [startup+1180.13 s] Raw data (loadavg): 1.04 1.00 0.98 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34950 0 0 0 117542 214 0 0 25 0 1 0 1785819973 147169280 34188 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 35930 34188 145 145 0 35785 0 [pid=12210] vsize: 143720 Current children cumulated CPU time (s) 1177.56 Current children cumulated vsize (Kb) 145844 [startup+1190.14 s] Raw data (loadavg): 1.04 1.00 0.98 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 35107 0 0 0 118539 216 0 0 25 0 1 0 1785819973 147795968 34345 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 36083 34345 145 145 0 35938 0 [pid=12210] vsize: 144332 Current children cumulated CPU time (s) 1187.55 Current children cumulated vsize (Kb) 146456 [startup+1200.14 s] Raw data (loadavg): 1.03 1.00 0.98 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 35169 0 0 0 119537 218 0 0 25 0 1 0 1785819973 148041728 34407 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 36143 34407 145 145 0 35998 0 [pid=12210] vsize: 144572 Current children cumulated CPU time (s) 1197.55 Current children cumulated vsize (Kb) 146696 [startup+1210.14 s] Raw data (loadavg): 1.03 1.00 0.98 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 35361 0 0 0 120533 219 0 0 25 0 1 0 1785819973 148811776 34599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 36331 34599 145 145 0 36186 0 [pid=12210] vsize: 145324 Current children cumulated CPU time (s) 1207.52 Current children cumulated vsize (Kb) 147448 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.14 s] Raw data (loadavg): 1.03 1.00 0.98 2/57 12210 Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12206/statm): 531 226 485 147 0 384 0 [pid=12206] vsize: 2124 Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 35361 0 0 0 120533 219 0 0 25 0 1 0 1785819973 148811776 34599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12210/statm): 36331 34599 145 145 0 36186 0 [pid=12210] vsize: 145324 Current children cumulated CPU time (s) 1207.52 Current children cumulated vsize (Kb) 147448 Sending SIGTERM to -12206 Sleeping 2 seconds One traced child (pid=12206) ended because it received signal 15 (SIGTERM) One traced child (pid=12210) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.21 CPU time (s): 1207.6 CPU user time (s): 1205.33 CPU system time (s): 2.26166 CPU usage (%): 99.784 Max. virtual memory (cumulated for all children) (Kb): 147448
ERROR: no interpretation found !