Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen2.opb |
MD5SUM | 30256c883dd8af773c334a2b26410bd9 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 9400 |
Biggest coefficient in the objective function | 2494038016 |
Number of bits for the biggest coefficient in the objective function | 32 |
Sum of the numbers in the objective function | 391862963250 |
Number of bits of the sum of numbers in the objective function | 39 |
Biggest number in a constraint | 2494038016 |
Number of bits of the biggest number in a constraint | 32 |
Biggest sum of numbers in a constraint | 391862963250 |
Number of bits of the biggest sum of numbers | 39 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 10680 |
Total number of constraints | 444 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 444 |
Minimum length of a constraint | 40 |
Maximum length of a constraint | 1700 |
LAUNCH ON wulflinc25 THE 2005-09-20 02:35:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3150 boxname=wulflinc25 idbench=806 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 30256c883dd8af773c334a2b26410bd9 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-degen2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-degen2.opb IDLAUNCH: 3150 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 921264 kB Buffers: 4436 kB Cached: 81072 kB SwapCached: 852 kB Active: 21588 kB Inactive: 66604 kB HighTotal: 131008 kB HighFree: 46452 kB LowTotal: 903652 kB LowFree: 874812 kB SwapTotal: 2097892 kB SwapFree: 2096524 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5720 kB Slab: 19400 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:55:41 (client local time) WITH STATUS 0 IN 1206.65 SECONDS stats: 3150 7 1206.65 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: 1514 maxlim: 182446 bits: 18/18 c ---[ 666]---> Adder-cost: 1514 maxlim: 103596 bits: 17/17 c ---[ 665]---> Adder-cost: 1168 maxlim: 90177 bits: 17/17 c ---[ 663]---> Sorter-cost: 1893 Base: 2 2 2 2 2 2 2 c ---[ 661]---> Sorter-cost: 1893 Base: 2 2 2 2 2 2 2 c ---[ 659]---> Adder-cost: 256 maxlim: 2167 bits: 13/12 c ---[ 657]---> Adder-cost: 256 maxlim: 2295 bits: 13/12 c ---[ 655]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 653]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 651]---> Sorter-cost: 1441 Base: 2 2 2 2 2 2 2 c ---[ 649]---> Sorter-cost: 1441 Base: 2 2 2 2 2 2 2 c ---[ 647]---> Adder-cost: 496 maxlim: 4335 bits: 13/13 c ---[ 645]---> Adder-cost: 528 maxlim: 4335 bits: 14/13 c ---[ 643]---> Sorter-cost: 1441 Base: 2 2 2 2 2 2 2 c ---[ 641]---> Sorter-cost: 1441 Base: 2 2 2 2 2 2 2 c ---[ 639]---> Adder-cost: 320 maxlim: 2805 bits: 13/12 c ---[ 637]---> Adder-cost: 320 maxlim: 2805 bits: 13/12 c ---[ 635]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 c ---[ 633]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 c ---[ 631]---> Adder-cost: 320 maxlim: 2805 bits: 13/12 c ---[ 629]---> Adder-cost: 336 maxlim: 2805 bits: 13/12 c ---[ 627]---> BDD-cost: 22 c ---[ 625]---> Adder-cost: 208 maxlim: 1785 bits: 12/11 c ---[ 623]---> Adder-cost: 208 maxlim: 1785 bits: 12/11 c ---[ 621]---> Adder-cost: 632 maxlim: 5228 bits: 14/13 c ---[ 619]---> Adder-cost: 600 maxlim: 4845 bits: 14/13 c ---[ 617]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 615]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 613]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 611]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 609]---> Adder-cost: 832 maxlim: 6375 bits: 14/13 c ---[ 607]---> Adder-cost: 848 maxlim: 6758 bits: 14/13 c ---[ 605]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 603]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 601]---> Sorter-cost: 1893 Base: 2 2 2 2 2 2 2 c ---[ 599]---> Sorter-cost: 1893 Base: 2 2 2 2 2 2 2 c ---[ 597]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 595]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 593]---> Sorter-cost: 280 Base: 2 2 2 2 2 2 2 c ---[ 591]---> Sorter-cost: 280 Base: 2 2 2 2 2 2 2 c ---[ 589]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 587]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 585]---> Adder-cost: 240 maxlim: 2040 bits: 12/11 c ---[ 583]---> Adder-cost: 224 maxlim: 2040 bits: 12/11 c ---[ 581]---> Adder-cost: 464 maxlim: 3825 bits: 13/12 c ---[ 579]---> Adder-cost: 480 maxlim: 4080 bits: 13/12 c ---[ 577]---> BDD-cost: 64 c ---[ 576]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 575]---> Sorter-cost: 294 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 574]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 573]---> Sorter-cost: 617 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 572]---> Sorter-cost: 703 Base: 2 2 2 2 2 2 2 7 c ---[ 571]---> Sorter-cost: 719 Base: 2 2 2 2 2 2 2 7 c ---[ 570]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 569]---> Sorter-cost: 1023 Base: 2 2 2 2 2 2 2 7 c ---[ 568]---> Sorter-cost: 1023 Base: 2 2 2 2 2 2 2 7 c ---[ 567]---> BDD-cost: 26 c ---[ 566]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 565]---> BDD-cost: 67 c ---[ 564]---> BDD-cost: 67 c ---[ 563]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 562]---> Sorter-cost: 933 Base: 2 2 2 2 2 2 2 7 c ---[ 561]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 560]---> Sorter-cost: 1652 Base: 2 2 2 2 2 2 2 7 c ---[ 559]---> Sorter-cost: 1303 Base: 2 2 2 2 2 2 2 7 c ---[ 558]---> BDD-cost: 68 c ---[ 557]---> BDD-cost: 67 c ---[ 556]---> BDD-cost: 67 c ---[ 555]---> BDD-cost: 68 c ---[ 554]---> BDD-cost: 67 c ---[ 553]---> BDD-cost: 67 c ---[ 552]---> Sorter-cost: 398 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 551]---> Sorter-cost: 394 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 550]---> Sorter-cost: 474 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 549]---> Sorter-cost: 728 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 548]---> Sorter-cost: 838 Base: 2 2 2 2 2 2 2 7 c ---[ 547]---> Sorter-cost: 854 Base: 2 2 2 2 2 2 2 7 c ---[ 546]---> Sorter-cost: 826 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 545]---> Sorter-cost: 936 Base: 2 2 2 2 2 2 2 7 c ---[ 544]---> Sorter-cost: 936 Base: 2 2 2 2 2 2 2 7 c ---[ 543]---> Adder-cost: 167 maxlim: 1529 bits: 12/11 c ---[ 542]---> Sorter-cost: 1815 Base: 2 2 2 2 2 2 2 7 c ---[ 541]---> Sorter-cost: 1815 Base: 2 2 2 2 2 2 2 7 c ---[ 540]---> Adder-cost: 217 maxlim: 2039 bits: 12/11 c ---[ 539]---> Adder-cost: 230 maxlim: 1911 bits: 12/11 c ---[ 538]---> Adder-cost: 230 maxlim: 2039 bits: 12/11 c ---[ 537]---> Adder-cost: 217 maxlim: 2294 bits: 13/12 c ---[ 536]---> Adder-cost: 224 maxlim: 2166 bits: 13/12 c ---[ 535]---> Adder-cost: 240 maxlim: 2294 bits: 13/12 c ---[ 534]---> Adder-cost: 262 maxlim: 3059 bits: 13/12 c ---[ 533]---> Adder-cost: 295 maxlim: 2931 bits: 13/12 c ---[ 532]---> Adder-cost: 311 maxlim: 3059 bits: 13/12 c ---[ 531]---> Adder-cost: 346 maxlim: 3314 bits: 13/12 c ---[ 530]---> Adder-cost: 361 maxlim: 3186 bits: 13/12 c ---[ 529]---> Adder-cost: 361 maxlim: 3314 bits: 13/12 c ---[ 528]---> Adder-cost: 346 maxlim: 3569 bits: 13/12 c ---[ 527]---> Adder-cost: 377 maxlim: 3441 bits: 13/12 c ---[ 526]---> Adder-cost: 393 maxlim: 3569 bits: 13/12 c ---[ 525]---> Adder-cost: 304 maxlim: 3824 bits: 13/12 c ---[ 524]---> Adder-cost: 323 maxlim: 3696 bits: 13/12 c ---[ 523]---> Adder-cost: 405 maxlim: 3824 bits: 13/12 c ---[ 522]---> BDD-cost: 68 c ---[ 521]---> BDD-cost: 67 c ---[ 520]---> BDD-cost: 67 c ---[ 519]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 518]---> Sorter-cost: 458 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 517]---> Sorter-cost: 474 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 516]---> Sorter-cost: 808 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 515]---> Sorter-cost: 918 Base: 2 2 2 2 2 2 2 7 c ---[ 514]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[ 513]---> Sorter-cost: 665 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 512]---> Sorter-cost: 751 Base: 2 2 2 2 2 2 2 7 c ---[ 511]---> Sorter-cost: 997 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 510]---> Sorter-cost: 1090 Base: 2 2 2 2 2 2 2 7 c ---[ 509]---> BDD-cost: 67 c ---[ 508]---> Sorter-cost: 474 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 507]---> Adder-cost: 167 maxlim: 1784 bits: 12/11 c ---[ 506]---> Sorter-cost: 1751 Base: 2 2 2 2 2 2 2 7 c ---[ 505]---> Sorter-cost: 751 Base: 2 2 2 2 2 2 2 7 c ---[ 504]---> Adder-cost: 199 maxlim: 2294 bits: 13/12 c ---[ 503]---> Adder-cost: 214 maxlim: 2294 bits: 13/12 c ---[ 502]---> Sorter-cost: 1070 Base: 2 2 2 2 2 2 2 7 c ---[ 501]---> Adder-cost: 225 maxlim: 2549 bits: 13/12 c ---[ 500]---> Adder-cost: 240 maxlim: 2549 bits: 13/12 c ---[ 499]---> Sorter-cost: 398 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 498]---> Sorter-cost: 394 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 497]---> BDD-cost: 68 c ---[ 496]---> BDD-cost: 67 c ---[ 495]---> Sorter-cost: 1302 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 494]---> Sorter-cost: 1359 Base: 2 2 2 2 2 2 2 7 c ---[ 493]---> Adder-cost: 185 maxlim: 1274 bits: 12/11 c ---[ 492]---> Adder-cost: 196 maxlim: 1274 bits: 12/11 c ---[ 491]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 490]---> BDD-cost: 68 c ---[ 489]---> BDD-cost: 67 c ---[ 488]---> BDD-cost: 67 c ---[ 487]---> Sorter-cost: 460 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 486]---> Sorter-cost: 456 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 485]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> Sorter-cost: 824 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 483]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[ 482]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[ 481]---> Sorter-cost: 1204 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 480]---> Sorter-cost: 1255 Base: 2 2 2 2 2 2 2 7 c ---[ 479]---> Sorter-cost: 1255 Base: 2 2 2 2 2 2 2 7 c ---[ 478]---> Adder-cost: 135 maxlim: 1274 bits: 12/11 c ---[ 477]---> Sorter-cost: 1720 Base: 2 2 2 2 2 2 2 7 c ---[ 476]---> Sorter-cost: 1720 Base: 2 2 2 2 2 2 2 7 c ---[ 475]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 474]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 473]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 472]---> Sorter-cost: 1088 Base: 2 2 2 2 2 2 2 7 c ---[ 471]---> Adder-cost: 149 maxlim: 764 bits: 11/10 c ---[ 470]---> BDD-cost: 67 c ---[ 469]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 468]---> Adder-cost: 249 maxlim: 1784 bits: 12/11 c ---[ 467]---> Adder-cost: 230 maxlim: 1657 bits: 12/11 c ---[ 466]---> Adder-cost: 210 maxlim: 2039 bits: 12/11 c ---[ 465]---> Adder-cost: 206 maxlim: 1912 bits: 12/11 c ---[ 464]---> Sorter-cost: 918 Base: 2 2 2 2 2 2 2 7 c ---[ 463]---> Adder-cost: 297 maxlim: 2167 bits: 13/12 c ---[ 462]---> Adder-cost: 294 maxlim: 2422 bits: 13/12 c ---[ 461]---> Adder-cost: 286 maxlim: 2677 bits: 13/12 c ---[ 460]---> Adder-cost: 269 maxlim: 2422 bits: 13/12 c ---[ 459]---> Sorter-cost: 1587 Base: 2 2 2 2 2 2 2 7 c ---[ 458]---> Adder-cost: 426 maxlim: 2804 bits: 13/12 c ---[ 457]---> Adder-cost: 456 maxlim: 3186 bits: 13/12 c ---[ 456]---> Adder-cost: 439 maxlim: 3059 bits: 13/12 c ---[ 455]---> BDD-cost: 66 c ---[ 454]---> BDD-cost: 65 c ---[ 453]---> BDD-cost: 67 c ---[ 452]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 451]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 450]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 449]---> BDD-cost: 25 c ---[ 448]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 447]---> BDD-cost: 68 c ---[ 446]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 445]---> Sorter-cost: 719 Base: 2 2 2 2 2 2 2 7 c ---[ 442]---> Sorter-cost: 479 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 441]---> Sorter-cost: 475 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 440]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 439]---> Adder-cost: 184 maxlim: 1912 bits: 12/11 c ---[ 438]---> Sorter-cost: 1605 Base: 2 2 2 2 2 2 2 7 c ---[ 437]---> Adder-cost: 185 maxlim: 1912 bits: 12/11 c ---[ 436]---> Adder-cost: 200 maxlim: 2167 bits: 13/12 c ---[ 435]---> Adder-cost: 184 maxlim: 1912 bits: 12/11 c ---[ 434]---> Adder-cost: 266 maxlim: 2677 bits: 13/12 c ---[ 433]---> Adder-cost: 279 maxlim: 2932 bits: 13/12 c ---[ 432]---> Adder-cost: 256 maxlim: 2677 bits: 13/12 c ---[ 431]---> Adder-cost: 314 maxlim: 2932 bits: 13/12 c ---[ 430]---> Adder-cost: 309 maxlim: 3187 bits: 13/12 c ---[ 429]---> Adder-cost: 222 maxlim: 3187 bits: 13/12 c ---[ 428]---> Adder-cost: 296 maxlim: 3569 bits: 13/12 c ---[ 427]---> Adder-cost: 339 maxlim: 3952 bits: 13/12 c ---[ 426]---> Adder-cost: 287 maxlim: 3442 bits: 13/12 c ---[ 425]---> Adder-cost: 258 maxlim: 3442 bits: 13/12 c ---[ 424]---> Adder-cost: 422 maxlim: 4079 bits: 13/12 c ---[ 423]---> Adder-cost: 442 maxlim: 4462 bits: 14/13 c ---[ 422]---> Adder-cost: 391 maxlim: 3952 bits: 13/12 c ---[ 421]---> Adder-cost: 421 maxlim: 4844 bits: 14/13 c ---[ 420]---> Adder-cost: 420 maxlim: 5227 bits: 14/13 c ---[ 419]---> Adder-cost: 490 maxlim: 4462 bits: 14/13 c ---[ 418]---> Adder-cost: 493 maxlim: 5609 bits: 14/13 c ---[ 417]---> Adder-cost: 470 maxlim: 5992 bits: 14/13 c ---[ 416]---> Adder-cost: 496 maxlim: 5227 bits: 14/13 c ---[ 415]---> Adder-cost: 553 maxlim: 5864 bits: 14/13 c ---[ 414]---> Adder-cost: 562 maxlim: 6247 bits: 14/13 c ---[ 413]---> Adder-cost: 610 maxlim: 5482 bits: 14/13 c ---[ 412]---> Adder-cost: 597 maxlim: 6119 bits: 14/13 c ---[ 411]---> Adder-cost: 598 maxlim: 6502 bits: 14/13 c ---[ 410]---> Adder-cost: 564 maxlim: 5737 bits: 14/13 c ---[ 409]---> BDD-cost: 27 c ---[ 408]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 407]---> BDD-cost: 67 c ---[ 406]---> BDD-cost: 67 c ---[ 405]---> BDD-cost: 68 c ---[ 404]---> BDD-cost: 67 c ---[ 403]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 402]---> Sorter-cost: 458 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 401]---> Sorter-cost: 792 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 400]---> Sorter-cost: 902 Base: 2 2 2 2 2 2 2 7 c ---[ 399]---> BDD-cost: 68 c ---[ 398]---> BDD-cost: 67 c ---[ 397]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 396]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 395]---> BDD-cost: 67 c ---[ 394]---> BDD-cost: 66 c ---[ 393]---> BDD-cost: 65 c ---[ 392]---> BDD-cost: 67 c ---[ 391]---> BDD-cost: 66 c ---[ 390]---> BDD-cost: 65 c ---[ 389]---> BDD-cost: 67 c ---[ 388]---> BDD-cost: 0 c ---[ 387]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 386]---> Sorter-cost: 458 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 385]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 384]---> BDD-cost: 68 c ---[ 383]---> BDD-cost: 67 c ---[ 382]---> BDD-cost: 67 c ---[ 381]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 380]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 379]---> Sorter-cost: 997 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 378]---> Sorter-cost: 1089 Base: 2 2 2 2 2 2 2 7 c ---[ 377]---> Sorter-cost: 752 Base: 2 2 2 2 2 2 2 7 c ---[ 376]---> BDD-cost: 67 c ---[ 374]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 373]---> Sorter-cost: 474 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 372]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 371]---> Adder-cost: 167 maxlim: 1275 bits: 12/11 c ---[ 370]---> Adder-cost: 184 maxlim: 1274 bits: 12/11 c ---[ 369]---> Adder-cost: 185 maxlim: 1785 bits: 12/11 c ---[ 368]---> Adder-cost: 182 maxlim: 1784 bits: 12/11 c ---[ 367]---> Adder-cost: 233 maxlim: 2040 bits: 12/11 c ---[ 366]---> Adder-cost: 240 maxlim: 2039 bits: 12/11 c ---[ 365]---> Sorter-cost: 900 Base: 2 2 2 2 2 2 2 7 c ---[ 364]---> Adder-cost: 228 maxlim: 2295 bits: 13/12 c ---[ 363]---> Adder-cost: 245 maxlim: 2294 bits: 13/12 c ---[ 362]---> Adder-cost: 410 maxlim: 2294 bits: 13/12 c ---[ 361]---> Adder-cost: 409 maxlim: 2549 bits: 13/12 c ---[ 360]---> Adder-cost: 304 maxlim: 2549 bits: 13/12 c ---[ 359]---> Adder-cost: 335 maxlim: 2804 bits: 13/12 c ---[ 358]---> BDD-cost: 65 c ---[ 357]---> BDD-cost: 67 c ---[ 355]---> BDD-cost: 35 c ---[ 353]---> BDD-cost: 35 c ---[ 351]---> BDD-cost: 35 c ---[ 349]---> BDD-cost: 35 c ---[ 347]---> BDD-cost: 35 c ---[ 345]---> BDD-cost: 35 c ---[ 343]---> BDD-cost: 35 c ---[ 341]---> BDD-cost: 35 c ---[ 339]---> BDD-cost: 35 c ---[ 337]---> BDD-cost: 35 c ---[ 335]---> BDD-cost: 35 c ---[ 333]---> BDD-cost: 35 c ---[ 331]---> BDD-cost: 35 c ---[ 329]---> BDD-cost: 35 c ---[ 327]---> BDD-cost: 35 c ---[ 325]---> BDD-cost: 35 c ---[ 323]---> BDD-cost: 35 c ---[ 321]---> BDD-cost: 35 c ---[ 319]---> BDD-cost: 76 c ---[ 317]---> BDD-cost: 76 c ---[ 315]---> BDD-cost: 35 c ---[ 313]---> BDD-cost: 35 c ---[ 311]---> BDD-cost: 35 c ---[ 309]---> BDD-cost: 35 c ---[ 307]---> BDD-cost: 35 c ---[ 305]---> BDD-cost: 35 c ---[ 303]---> BDD-cost: 35 c ---[ 301]---> BDD-cost: 35 c ---[ 299]---> BDD-cost: 35 c ---[ 297]---> BDD-cost: 35 c ---[ 295]---> BDD-cost: 35 c ---[ 293]---> BDD-cost: 35 c ---[ 291]---> BDD-cost: 76 c ---[ 289]---> BDD-cost: 35 c ---[ 287]---> BDD-cost: 35 c ---[ 285]---> BDD-cost: 35 c ---[ 283]---> BDD-cost: 35 c ---[ 281]---> BDD-cost: 35 c ---[ 279]---> BDD-cost: 35 c ---[ 277]---> BDD-cost: 35 c ---[ 275]---> BDD-cost: 35 c ---[ 273]---> BDD-cost: 35 c ---[ 271]---> BDD-cost: 35 c ---[ 269]---> BDD-cost: 35 c ---[ 267]---> BDD-cost: 35 c ---[ 265]---> BDD-cost: 35 c ---[ 263]---> BDD-cost: 35 c ---[ 261]---> BDD-cost: 35 c ---[ 259]---> BDD-cost: 35 c ---[ 257]---> BDD-cost: 35 c ---[ 255]---> BDD-cost: 35 c ---[ 253]---> BDD-cost: 35 c ---[ 251]---> BDD-cost: 35 c ---[ 249]---> BDD-cost: 35 c ---[ 247]---> BDD-cost: 35 c ---[ 245]---> BDD-cost: 35 c ---[ 243]---> BDD-cost: 35 c ---[ 241]---> BDD-cost: 35 c ---[ 239]---> BDD-cost: 35 c ---[ 237]---> BDD-cost: 76 c ---[ 235]---> BDD-cost: 76 c ---[ 233]---> BDD-cost: 76 c ---[ 231]---> BDD-cost: 76 c ---[ 229]---> BDD-cost: 76 c ---[ 227]---> BDD-cost: 76 c ---[ 225]---> BDD-cost: 76 c ---[ 223]---> BDD-cost: 76 c ---[ 221]---> BDD-cost: 76 c ---[ 219]---> BDD-cost: 76 c ---[ 217]---> BDD-cost: 76 c ---[ 215]---> BDD-cost: 76 c ---[ 213]---> BDD-cost: 76 c ---[ 211]---> BDD-cost: 76 c ---[ 209]---> BDD-cost: 76 c ---[ 207]---> BDD-cost: 76 c ---[ 205]---> BDD-cost: 76 c ---[ 203]---> BDD-cost: 76 c ---[ 201]---> BDD-cost: 76 c ---[ 199]---> BDD-cost: 76 c ---[ 197]---> BDD-cost: 76 c ---[ 195]---> BDD-cost: 76 c ---[ 193]---> BDD-cost: 76 c ---[ 191]---> BDD-cost: 76 c ---[ 189]---> BDD-cost: 76 c ---[ 187]---> BDD-cost: 76 c ---[ 185]---> BDD-cost: 76 c ---[ 183]---> BDD-cost: 76 c ---[ 181]---> BDD-cost: 76 c ---[ 179]---> BDD-cost: 76 c ---[ 177]---> BDD-cost: 76 c ---[ 175]---> BDD-cost: 76 c ---[ 173]---> BDD-cost: 76 c ---[ 171]---> BDD-cost: 76 c ---[ 169]---> BDD-cost: 76 c ---[ 167]---> BDD-cost: 76 c ---[ 165]---> BDD-cost: 35 c ---[ 163]---> BDD-cost: 76 c ---[ 161]---> BDD-cost: 76 c ---[ 159]---> BDD-cost: 76 c ---[ 157]---> BDD-cost: 76 c ---[ 155]---> BDD-cost: 76 c ---[ 153]---> BDD-cost: 76 c ---[ 151]---> BDD-cost: 76 c ---[ 149]---> BDD-cost: 76 c ---[ 147]---> BDD-cost: 76 c ---[ 145]---> BDD-cost: 76 c ---[ 143]---> BDD-cost: 76 c ---[ 141]---> BDD-cost: 76 c ---[ 139]---> BDD-cost: 76 c ---[ 137]---> BDD-cost: 76 c ---[ 135]---> BDD-cost: 76 c ---[ 133]---> BDD-cost: 76 c ---[ 131]---> BDD-cost: 76 c ---[ 129]---> BDD-cost: 76 c ---[ 127]---> BDD-cost: 76 c ---[ 125]---> BDD-cost: 76 c ---[ 123]---> BDD-cost: 76 c ---[ 121]---> BDD-cost: 76 c ---[ 119]---> BDD-cost: 76 c ---[ 117]---> BDD-cost: 76 c ---[ 115]---> BDD-cost: 76 c ---[ 113]---> BDD-cost: 76 c ---[ 111]---> BDD-cost: 35 c ---[ 109]---> BDD-cost: 76 c ---[ 107]---> BDD-cost: 76 c ---[ 105]---> BDD-cost: 76 c ---[ 103]---> BDD-cost: 76 c ---[ 101]---> BDD-cost: 76 c ---[ 99]---> BDD-cost: 76 c ---[ 97]---> BDD-cost: 76 c ---[ 95]---> BDD-cost: 76 c ---[ 93]---> BDD-cost: 76 c ---[ 91]---> BDD-cost: 76 c ---[ 89]---> BDD-cost: 76 c ---[ 87]---> BDD-cost: 76 c ---[ 85]---> BDD-cost: 76 c ---[ 83]---> BDD-cost: 76 c ---[ 81]---> BDD-cost: 76 c ---[ 79]---> BDD-cost: 76 c ---[ 77]---> BDD-cost: 76 c ---[ 75]---> BDD-cost: 76 c ---[ 73]---> BDD-cost: 76 c ---[ 71]---> BDD-cost: 76 c ---[ 69]---> BDD-cost: 76 c ---[ 67]---> BDD-cost: 76 c ---[ 65]---> BDD-cost: 76 c ---[ 63]---> BDD-cost: 76 c ---[ 61]---> BDD-cost: 76 c ---[ 59]---> BDD-cost: 76 c ---[ 57]---> BDD-cost: 76 c ---[ 55]---> BDD-cost: 76 c ---[ 53]---> BDD-cost: 76 c ---[ 51]---> BDD-cost: 76 c ---[ 49]---> BDD-cost: 76 c ---[ 47]---> BDD-cost: 76 c ---[ 45]---> BDD-cost: 76 c ---[ 43]---> BDD-cost: 76 c ---[ 41]---> BDD-cost: 76 c ---[ 39]---> BDD-cost: 76 c ---[ 37]---> BDD-cost: 76 c ---[ 35]---> BDD-cost: 76 c ---[ 33]---> BDD-cost: 76 c ---[ 31]---> BDD-cost: 35 c ---[ 29]---> BDD-cost: 35 c ---[ 27]---> BDD-cost: 76 c ---[ 25]---> BDD-cost: 76 c ---[ 23]---> BDD-cost: 76 c ---[ 21]---> BDD-cost: 76 c ---[ 19]---> BDD-cost: 76 c ---[ 17]---> BDD-cost: 76 c ---[ 15]---> BDD-cost: 76 c ---[ 13]---> BDD-cost: 76 c ---[ 11]---> BDD-cost: 76 c ---[ 9]---> BDD-cost: 76 c ---[ 7]---> BDD-cost: 76 c ---[ 5]---> BDD-cost: 76 c ---[ 3]---> BDD-cost: 76 c ---[ 2]---> BDD-cost: 20 c ---[ 1]---> BDD-cost: 19 c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 517734 1531647 | 172578 0 0 nan | 0.000 % | c | 100 | 517717 1531609 | 189835 99 453 4.6 | 5.871 % | c | 250 | 517717 1531609 | 208819 249 1150 4.6 | 5.871 % | c | 476 | 517679 1531525 | 229701 463 2089 4.5 | 5.879 % | c | 813 | 517675 1531517 | 252671 798 4142 5.2 | 5.881 % | c | 1319 | 517561 1531264 | 277938 1289 7041 5.5 | 5.903 % | c | 2078 | 517493 1531112 | 305732 2040 10468 5.1 | 5.915 % | c | 3217 | 517318 1530722 | 336305 3153 16763 5.3 | 5.949 % | c | 4925 | 517256 1530584 | 369936 4855 26338 5.4 | 5.962 % | c | 7487 | 517100 1530237 | 406929 7399 44864 6.1 | 5.992 % | c | 11331 | 516686 1529314 | 447622 11187 68385 6.1 | 6.072 % | c | 17097 | 516269 1528373 | 492385 16897 109055 6.5 | 6.153 % | c | 25746 | 516084 1527923 | 541623 25523 328866 12.9 | 6.186 % | c | 38720 | 515683 1526983 | 595786 38439 440277 11.5 | 6.260 % | c | 58181 | 515503 1526540 | 655364 57867 1081332 18.7 | 6.291 % | c | 87374 | 515359 1526115 | 720901 87039 2438431 28.0 | 6.314 % | c | 131163 | 515177 1525635 | 792991 130797 3879866 29.7 | 6.345 % | c | 196847 | 514859 1524856 | 872290 196429 7837911 39.9 | 6.401 % | c | 295373 | 514520 1523952 | 959519 294904 11429805 38.8 | 6.460 % | c | 443163 | 514380 1523577 | 1055471 442666 19716307 44.5 | 6.480 % |
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/26656/stat): 26656 (minisat+_script) R 26655 26656 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855007608 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/26656/statm): 174 3 169 147 0 27 0 [pid=26656] 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=26657 New process pid=26658 New process pid=26659 One traced child (pid=26658) exited with status: 0 execve syscall for /bin/sed executable 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=26659) exited with status: 0 One traced child (pid=26657) exited with status: 0 New process pid=26660 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-degen2.opb [startup+10.0036 s] Raw data (loadavg): 0.93 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12672 0 0 0 884 55 0 0 25 0 1 0 1855007613 60432384 12296 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 14754 12296 145 145 0 14609 0 [pid=26660] vsize: 59016 Current children cumulated CPU time (s) 9.39 Current children cumulated vsize (Kb) 61140 [startup+20.0052 s] Raw data (loadavg): 0.94 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12769 0 0 0 1883 56 0 0 25 0 1 0 1855007613 60821504 12393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 14849 12393 145 145 0 14704 0 [pid=26660] vsize: 59396 Current children cumulated CPU time (s) 19.39 Current children cumulated vsize (Kb) 61520 [startup+30.0058 s] Raw data (loadavg): 0.95 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12867 0 0 0 2881 56 0 0 25 0 1 0 1855007613 61165568 12491 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 14933 12491 145 145 0 14788 0 [pid=26660] vsize: 59732 Current children cumulated CPU time (s) 29.37 Current children cumulated vsize (Kb) 61856 [startup+40.0064 s] Raw data (loadavg): 0.96 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12918 0 0 0 3880 57 0 0 25 0 1 0 1855007613 61370368 12542 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 14983 12542 145 145 0 14838 0 [pid=26660] vsize: 59932 Current children cumulated CPU time (s) 39.37 Current children cumulated vsize (Kb) 62056 [startup+50.0069 s] Raw data (loadavg): 0.96 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12966 0 0 0 4880 57 0 0 25 0 1 0 1855007613 61538304 12590 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 15024 12590 145 145 0 14879 0 [pid=26660] vsize: 60096 Current children cumulated CPU time (s) 49.37 Current children cumulated vsize (Kb) 62220 [startup+60.0076 s] Raw data (loadavg): 0.97 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13018 0 0 0 5879 57 0 0 25 0 1 0 1855007613 61726720 12642 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 15070 12642 145 145 0 14925 0 [pid=26660] vsize: 60280 Current children cumulated CPU time (s) 59.36 Current children cumulated vsize (Kb) 62404 [startup+70.0082 s] Raw data (loadavg): 0.97 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13081 0 0 0 6879 58 0 0 25 0 1 0 1855007613 62009344 12705 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 15139 12705 145 145 0 14994 0 [pid=26660] vsize: 60556 Current children cumulated CPU time (s) 69.37 Current children cumulated vsize (Kb) 62680 [startup+80.0088 s] Raw data (loadavg): 0.98 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13337 0 0 0 7874 59 0 0 25 0 1 0 1855007613 63033344 12961 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 15389 12961 145 145 0 15244 0 [pid=26660] vsize: 61556 Current children cumulated CPU time (s) 79.33 Current children cumulated vsize (Kb) 63680 [startup+90.0094 s] Raw data (loadavg): 0.98 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13385 0 0 0 8872 60 0 0 25 0 1 0 1855007613 63217664 13009 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 15434 13009 145 145 0 15289 0 [pid=26660] vsize: 61736 Current children cumulated CPU time (s) 89.32 Current children cumulated vsize (Kb) 63860 [startup+100.01 s] Raw data (loadavg): 0.98 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13442 0 0 0 9870 61 0 0 25 0 1 0 1855007613 63438848 13066 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 15488 13066 145 145 0 15343 0 [pid=26660] vsize: 61952 Current children cumulated CPU time (s) 99.31 Current children cumulated vsize (Kb) 64076 [startup+110.012 s] Raw data (loadavg): 0.98 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13509 0 0 0 10869 62 0 0 25 0 1 0 1855007613 63832064 13133 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 15584 13133 145 145 0 15439 0 [pid=26660] vsize: 62336 Current children cumulated CPU time (s) 109.31 Current children cumulated vsize (Kb) 64460 [startup+120.012 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13559 0 0 0 11868 62 0 0 25 0 1 0 1855007613 64024576 13183 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 15631 13183 145 145 0 15486 0 [pid=26660] vsize: 62524 Current children cumulated CPU time (s) 119.3 Current children cumulated vsize (Kb) 64648 [startup+130.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13613 0 0 0 12866 63 0 0 25 0 1 0 1855007613 64233472 13237 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 15682 13237 145 145 0 15537 0 [pid=26660] vsize: 62728 Current children cumulated CPU time (s) 129.29 Current children cumulated vsize (Kb) 64852 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13670 0 0 0 13864 64 0 0 25 0 1 0 1855007613 64454656 13294 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 15736 13294 145 145 0 15591 0 [pid=26660] vsize: 62944 Current children cumulated CPU time (s) 139.28 Current children cumulated vsize (Kb) 65068 [startup+150.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13825 0 0 0 14862 66 0 0 25 0 1 0 1855007613 65069056 13449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 15886 13449 145 145 0 15741 0 [pid=26660] vsize: 63544 Current children cumulated CPU time (s) 149.28 Current children cumulated vsize (Kb) 65668 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14132 0 0 0 15856 68 0 0 25 0 1 0 1855007613 66301952 13756 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 16187 13756 145 145 0 16042 0 [pid=26660] vsize: 64748 Current children cumulated CPU time (s) 159.24 Current children cumulated vsize (Kb) 66872 [startup+170.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14574 0 0 0 16849 71 0 0 25 0 1 0 1855007613 68087808 14198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 16623 14198 145 145 0 16478 0 [pid=26660] vsize: 66492 Current children cumulated CPU time (s) 169.2 Current children cumulated vsize (Kb) 68616 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14713 0 0 0 17846 73 0 0 25 0 1 0 1855007613 68640768 14337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 16758 14337 145 145 0 16613 0 [pid=26660] vsize: 67032 Current children cumulated CPU time (s) 179.19 Current children cumulated vsize (Kb) 69156 [startup+190.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14825 0 0 0 18844 74 0 0 25 0 1 0 1855007613 69349376 14449 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 16931 14449 145 145 0 16786 0 [pid=26660] vsize: 67724 Current children cumulated CPU time (s) 189.18 Current children cumulated vsize (Kb) 69848 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14947 0 0 0 19842 76 0 0 25 0 1 0 1855007613 69779456 14571 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 17036 14571 145 145 0 16891 0 [pid=26660] vsize: 68144 Current children cumulated CPU time (s) 199.18 Current children cumulated vsize (Kb) 70268 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 15757 0 0 0 20828 83 0 0 25 0 1 0 1855007613 73052160 15381 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 17835 15381 145 145 0 17690 0 [pid=26660] vsize: 71340 Current children cumulated CPU time (s) 209.11 Current children cumulated vsize (Kb) 73464 [startup+220.022 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 16441 0 0 0 21815 88 0 0 25 0 1 0 1855007613 75816960 16065 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 18510 16065 145 145 0 18365 0 [pid=26660] vsize: 74040 Current children cumulated CPU time (s) 219.03 Current children cumulated vsize (Kb) 76164 [startup+230.023 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 16566 0 0 0 22812 90 0 0 25 0 1 0 1855007613 76312576 16190 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 18631 16190 145 145 0 18486 0 [pid=26660] vsize: 74524 Current children cumulated CPU time (s) 229.02 Current children cumulated vsize (Kb) 76648 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 16656 0 0 0 23810 92 0 0 25 0 1 0 1855007613 76664832 16280 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 18717 16280 145 145 0 18572 0 [pid=26660] vsize: 74868 Current children cumulated CPU time (s) 239.02 Current children cumulated vsize (Kb) 76992 [startup+250.026 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 16898 0 0 0 24805 93 0 0 25 0 1 0 1855007613 77635584 16522 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 18954 16522 145 145 0 18809 0 [pid=26660] vsize: 75816 Current children cumulated CPU time (s) 248.98 Current children cumulated vsize (Kb) 77940 [startup+260.027 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 17238 0 0 0 25799 97 0 0 25 0 1 0 1855007613 78999552 16862 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 19287 16862 145 145 0 19142 0 [pid=26660] vsize: 77148 Current children cumulated CPU time (s) 258.96 Current children cumulated vsize (Kb) 79272 [startup+270.027 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 17633 0 0 0 26791 99 0 0 25 0 1 0 1855007613 80588800 17257 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 19675 17257 145 145 0 19530 0 [pid=26660] vsize: 78700 Current children cumulated CPU time (s) 268.9 Current children cumulated vsize (Kb) 80824 [startup+280.028 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 17904 0 0 0 27786 102 0 0 25 0 1 0 1855007613 81670144 17528 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 19939 17528 145 145 0 19794 0 [pid=26660] vsize: 79756 Current children cumulated CPU time (s) 278.88 Current children cumulated vsize (Kb) 81880 [startup+290.028 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18097 0 0 0 28783 103 0 0 25 0 1 0 1855007613 82964480 17721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 20255 17721 145 145 0 20110 0 [pid=26660] vsize: 81020 Current children cumulated CPU time (s) 288.86 Current children cumulated vsize (Kb) 83144 [startup+300.029 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18202 0 0 0 29780 104 0 0 25 0 1 0 1855007613 83382272 17826 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 20357 17826 145 145 0 20212 0 [pid=26660] vsize: 81428 Current children cumulated CPU time (s) 298.84 Current children cumulated vsize (Kb) 83552 [startup+310.031 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18284 0 0 0 30779 105 0 0 25 0 1 0 1855007613 83705856 17908 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 20436 17908 145 145 0 20291 0 [pid=26660] vsize: 81744 Current children cumulated CPU time (s) 308.84 Current children cumulated vsize (Kb) 83868 [startup+320.031 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18349 0 0 0 31777 106 0 0 25 0 1 0 1855007613 83963904 17973 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 20499 17973 145 145 0 20354 0 [pid=26660] vsize: 81996 Current children cumulated CPU time (s) 318.83 Current children cumulated vsize (Kb) 84120 [startup+330.032 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18377 0 0 0 32776 106 0 0 25 0 1 0 1855007613 84070400 18001 4294967295 134512640 135094434 3221224432 3221223072 134562076 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 20525 18001 145 145 0 20380 0 [pid=26660] vsize: 82100 Current children cumulated CPU time (s) 328.82 Current children cumulated vsize (Kb) 84224 [startup+340.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18447 0 0 0 33774 108 0 0 25 0 1 0 1855007613 84344832 18071 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 20592 18071 145 145 0 20447 0 [pid=26660] vsize: 82368 Current children cumulated CPU time (s) 338.82 Current children cumulated vsize (Kb) 84492 [startup+350.034 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 19008 0 0 0 34764 112 0 0 25 0 1 0 1855007613 86614016 18632 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 21146 18632 145 145 0 21001 0 [pid=26660] vsize: 84584 Current children cumulated CPU time (s) 348.76 Current children cumulated vsize (Kb) 86708 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 19225 0 0 0 35760 114 0 0 25 0 1 0 1855007613 87486464 18849 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 21359 18849 145 145 0 21214 0 [pid=26660] vsize: 85436 Current children cumulated CPU time (s) 358.74 Current children cumulated vsize (Kb) 87560 [startup+370.036 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 19522 0 0 0 36756 115 0 0 25 0 1 0 1855007613 88678400 19146 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 21650 19146 145 145 0 21505 0 [pid=26660] vsize: 86600 Current children cumulated CPU time (s) 368.71 Current children cumulated vsize (Kb) 88724 [startup+380.036 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 19915 0 0 0 37749 118 0 0 25 0 1 0 1855007613 90267648 19539 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 22038 19539 145 145 0 21893 0 [pid=26660] vsize: 88152 Current children cumulated CPU time (s) 378.67 Current children cumulated vsize (Kb) 90276 [startup+390.037 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 20262 0 0 0 38743 120 0 0 25 0 1 0 1855007613 91676672 19886 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 22382 19886 145 145 0 22237 0 [pid=26660] vsize: 89528 Current children cumulated CPU time (s) 388.63 Current children cumulated vsize (Kb) 91652 [startup+400.038 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 20605 0 0 0 39738 122 0 0 23 0 1 0 1855007613 93061120 20229 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 22720 20229 145 145 0 22575 0 [pid=26660] vsize: 90880 Current children cumulated CPU time (s) 398.6 Current children cumulated vsize (Kb) 93004 [startup+410.039 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 20962 0 0 0 40730 126 0 0 25 0 1 0 1855007613 94507008 20586 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 23073 20586 145 145 0 22928 0 [pid=26660] vsize: 92292 Current children cumulated CPU time (s) 408.56 Current children cumulated vsize (Kb) 94416 [startup+420.04 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 21289 0 0 0 41723 129 0 0 25 0 1 0 1855007613 95834112 20913 4294967295 134512640 135094434 3221224432 3221223024 134556906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 23397 20913 145 145 0 23252 0 [pid=26660] vsize: 93588 Current children cumulated CPU time (s) 418.52 Current children cumulated vsize (Kb) 95712 [startup+430.041 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 21626 0 0 0 42718 131 0 0 25 0 1 0 1855007613 97210368 21250 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 23733 21250 145 145 0 23588 0 [pid=26660] vsize: 94932 Current children cumulated CPU time (s) 428.49 Current children cumulated vsize (Kb) 97056 [startup+440.041 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 21927 0 0 0 43711 133 0 0 25 0 1 0 1855007613 98422784 21551 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 24029 21551 145 145 0 23884 0 [pid=26660] vsize: 96116 Current children cumulated CPU time (s) 438.44 Current children cumulated vsize (Kb) 98240 [startup+450.042 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 22221 0 0 0 44707 135 0 0 25 0 1 0 1855007613 99639296 21845 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 24326 21845 145 145 0 24181 0 [pid=26660] vsize: 97304 Current children cumulated CPU time (s) 448.42 Current children cumulated vsize (Kb) 99428 [startup+460.044 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 22493 0 0 0 45702 137 0 0 25 0 1 0 1855007613 100753408 22117 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 24598 22117 145 145 0 24453 0 [pid=26660] vsize: 98392 Current children cumulated CPU time (s) 458.39 Current children cumulated vsize (Kb) 100516 [startup+470.044 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 22817 0 0 0 46696 140 0 0 25 0 1 0 1855007613 102064128 22441 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 24918 22441 145 145 0 24773 0 [pid=26660] vsize: 99672 Current children cumulated CPU time (s) 468.36 Current children cumulated vsize (Kb) 101796 [startup+480.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23295 0 0 0 47688 144 0 0 25 0 1 0 1855007613 103997440 22919 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 25390 22919 145 145 0 25245 0 [pid=26660] vsize: 101560 Current children cumulated CPU time (s) 478.32 Current children cumulated vsize (Kb) 103684 [startup+490.046 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23468 0 0 0 48684 145 0 0 25 0 1 0 1855007613 104697856 23092 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 25561 23092 145 145 0 25416 0 [pid=26660] vsize: 102244 Current children cumulated CPU time (s) 488.29 Current children cumulated vsize (Kb) 104368 [startup+500.047 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23518 0 0 0 49684 146 0 0 25 0 1 0 1855007613 104902656 23142 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 25611 23142 145 145 0 25466 0 [pid=26660] vsize: 102444 Current children cumulated CPU time (s) 498.3 Current children cumulated vsize (Kb) 104568 [startup+510.049 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23573 0 0 0 50682 146 0 0 25 0 1 0 1855007613 105119744 23197 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 25664 23197 145 145 0 25519 0 [pid=26660] vsize: 102656 Current children cumulated CPU time (s) 508.28 Current children cumulated vsize (Kb) 104780 [startup+520.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23643 0 0 0 51681 148 0 0 25 0 1 0 1855007613 105394176 23267 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 25731 23267 145 145 0 25586 0 [pid=26660] vsize: 102924 Current children cumulated CPU time (s) 518.29 Current children cumulated vsize (Kb) 105048 [startup+530.051 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23731 0 0 0 52679 148 0 0 25 0 1 0 1855007613 105746432 23355 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 25817 23355 145 145 0 25672 0 [pid=26660] vsize: 103268 Current children cumulated CPU time (s) 528.27 Current children cumulated vsize (Kb) 105392 [startup+540.053 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23770 0 0 0 53678 149 0 0 25 0 1 0 1855007613 105893888 23394 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 25853 23394 145 145 0 25708 0 [pid=26660] vsize: 103412 Current children cumulated CPU time (s) 538.27 Current children cumulated vsize (Kb) 105536 [startup+550.053 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23844 0 0 0 54676 150 0 0 25 0 1 0 1855007613 106184704 23468 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 25924 23468 145 145 0 25779 0 [pid=26660] vsize: 103696 Current children cumulated CPU time (s) 548.26 Current children cumulated vsize (Kb) 105820 [startup+560.055 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23927 0 0 0 55675 151 0 0 25 0 1 0 1855007613 106512384 23551 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 26004 23551 145 145 0 25859 0 [pid=26660] vsize: 104016 Current children cumulated CPU time (s) 558.26 Current children cumulated vsize (Kb) 106140 [startup+570.055 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 24668 0 0 0 56663 156 0 0 25 0 1 0 1855007613 109518848 24292 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 26738 24292 145 145 0 26593 0 [pid=26660] vsize: 106952 Current children cumulated CPU time (s) 568.19 Current children cumulated vsize (Kb) 109076 [startup+580.056 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 25129 0 0 0 57655 160 0 0 25 0 1 0 1855007613 111382528 24753 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 27193 24753 145 145 0 27048 0 [pid=26660] vsize: 108772 Current children cumulated CPU time (s) 578.15 Current children cumulated vsize (Kb) 110896 [startup+590.058 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 25328 0 0 0 58651 162 0 0 25 0 1 0 1855007613 112177152 24952 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 27387 24952 145 145 0 27242 0 [pid=26660] vsize: 109548 Current children cumulated CPU time (s) 588.13 Current children cumulated vsize (Kb) 111672 [startup+600.058 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 25711 0 0 0 59643 166 0 0 25 0 1 0 1855007613 113717248 25335 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 27763 25335 145 145 0 27618 0 [pid=26660] vsize: 111052 Current children cumulated CPU time (s) 598.09 Current children cumulated vsize (Kb) 113176 [startup+610.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 25910 0 0 0 60638 168 0 0 25 0 1 0 1855007613 114515968 25534 4294967295 134512640 135094434 3221224432 3221223024 134557251 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 27958 25534 145 145 0 27813 0 [pid=26660] vsize: 111832 Current children cumulated CPU time (s) 608.06 Current children cumulated vsize (Kb) 113956 [startup+620.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 26323 0 0 0 61629 173 0 0 25 0 1 0 1855007613 117231616 25947 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 28621 25947 145 145 0 28476 0 [pid=26660] vsize: 114484 Current children cumulated CPU time (s) 618.02 Current children cumulated vsize (Kb) 116608 [startup+630.061 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 26474 0 0 0 62626 175 0 0 25 0 1 0 1855007613 117833728 26098 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 28768 26098 145 145 0 28623 0 [pid=26660] vsize: 115072 Current children cumulated CPU time (s) 628.01 Current children cumulated vsize (Kb) 117196 [startup+640.063 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 26684 0 0 0 63622 177 0 0 25 0 1 0 1855007613 118673408 26308 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 28973 26308 145 145 0 28828 0 [pid=26660] vsize: 115892 Current children cumulated CPU time (s) 637.99 Current children cumulated vsize (Kb) 118016 [startup+650.063 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 26894 0 0 0 64618 179 0 0 25 0 1 0 1855007613 119513088 26518 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 29178 26518 145 145 0 29033 0 [pid=26660] vsize: 116712 Current children cumulated CPU time (s) 647.97 Current children cumulated vsize (Kb) 118836 [startup+660.065 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27015 0 0 0 65616 181 0 0 25 0 1 0 1855007613 120000512 26639 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 29297 26639 145 145 0 29152 0 [pid=26660] vsize: 117188 Current children cumulated CPU time (s) 657.97 Current children cumulated vsize (Kb) 119312 [startup+670.065 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27181 0 0 0 66612 183 0 0 25 0 1 0 1855007613 120664064 26805 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 29459 26805 145 145 0 29314 0 [pid=26660] vsize: 117836 Current children cumulated CPU time (s) 667.95 Current children cumulated vsize (Kb) 119960 [startup+680.066 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27302 0 0 0 67610 185 0 0 25 0 1 0 1855007613 121139200 26926 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 29575 26926 145 145 0 29430 0 [pid=26660] vsize: 118300 Current children cumulated CPU time (s) 677.95 Current children cumulated vsize (Kb) 120424 [startup+690.067 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27528 0 0 0 68605 187 0 0 25 0 1 0 1855007613 122028032 27152 4294967295 134512640 135094434 3221224432 3221223000 134538517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 29792 27152 145 145 0 29647 0 [pid=26660] vsize: 119168 Current children cumulated CPU time (s) 687.92 Current children cumulated vsize (Kb) 121292 [startup+700.068 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27633 0 0 0 69603 188 0 0 25 0 1 0 1855007613 122441728 27257 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 29893 27257 145 145 0 29748 0 [pid=26660] vsize: 119572 Current children cumulated CPU time (s) 697.91 Current children cumulated vsize (Kb) 121696 [startup+710.069 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27687 0 0 0 70601 189 0 0 25 0 1 0 1855007613 122654720 27311 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 29945 27311 145 145 0 29800 0 [pid=26660] vsize: 119780 Current children cumulated CPU time (s) 707.9 Current children cumulated vsize (Kb) 121904 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 28168 0 0 0 71592 194 0 0 25 0 1 0 1855007613 124588032 27792 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 30417 27792 145 145 0 30272 0 [pid=26660] vsize: 121668 Current children cumulated CPU time (s) 717.86 Current children cumulated vsize (Kb) 123792 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 28768 0 0 0 72582 198 0 0 25 0 1 0 1855007613 127025152 28392 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 31012 28392 145 145 0 30867 0 [pid=26660] vsize: 124048 Current children cumulated CPU time (s) 727.8 Current children cumulated vsize (Kb) 126172 [startup+740.072 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 29275 0 0 0 73571 202 0 0 25 0 1 0 1855007613 129089536 28899 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 31516 28899 145 145 0 31371 0 [pid=26660] vsize: 126064 Current children cumulated CPU time (s) 737.73 Current children cumulated vsize (Kb) 128188 [startup+750.072 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 29761 0 0 0 74562 206 0 0 25 0 1 0 1855007613 131063808 29385 4294967295 134512640 135094434 3221224432 3221223088 134561666 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 31998 29385 145 145 0 31853 0 [pid=26660] vsize: 127992 Current children cumulated CPU time (s) 747.68 Current children cumulated vsize (Kb) 130116 [startup+760.074 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 30224 0 0 0 75554 209 0 0 25 0 1 0 1855007613 132939776 29848 4294967295 134512640 135094434 3221224432 3221223072 134562225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 32456 29848 145 145 0 32311 0 [pid=26660] vsize: 129824 Current children cumulated CPU time (s) 757.63 Current children cumulated vsize (Kb) 131948 [startup+770.075 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 30653 0 0 0 76545 213 0 0 25 0 1 0 1855007613 134688768 30277 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 32883 30277 145 145 0 32738 0 [pid=26660] vsize: 131532 Current children cumulated CPU time (s) 767.58 Current children cumulated vsize (Kb) 133656 [startup+780.076 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 31058 0 0 0 77540 215 0 0 25 0 1 0 1855007613 136359936 30682 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 33291 30682 145 145 0 33146 0 [pid=26660] vsize: 133164 Current children cumulated CPU time (s) 777.55 Current children cumulated vsize (Kb) 135288 [startup+790.077 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 31459 0 0 0 78533 218 0 0 25 0 1 0 1855007613 137998336 31083 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 33691 31083 145 145 0 33546 0 [pid=26660] vsize: 134764 Current children cumulated CPU time (s) 787.51 Current children cumulated vsize (Kb) 136888 [startup+800.077 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 31870 0 0 0 79528 220 0 0 25 0 1 0 1855007613 139681792 31494 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 34102 31494 145 145 0 33957 0 [pid=26660] vsize: 136408 Current children cumulated CPU time (s) 797.48 Current children cumulated vsize (Kb) 138532 [startup+810.079 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 32235 0 0 0 80522 222 0 0 25 0 1 0 1855007613 141180928 31859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 34468 31859 145 145 0 34323 0 [pid=26660] vsize: 137872 Current children cumulated CPU time (s) 807.44 Current children cumulated vsize (Kb) 139996 [startup+820.079 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 32585 0 0 0 81518 224 0 0 25 0 1 0 1855007613 142606336 32209 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 34816 32209 145 145 0 34671 0 [pid=26660] vsize: 139264 Current children cumulated CPU time (s) 817.42 Current children cumulated vsize (Kb) 141388 [startup+830.08 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 32825 0 0 0 82514 226 0 0 25 0 1 0 1855007613 143572992 32449 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 35052 32449 145 145 0 34907 0 [pid=26660] vsize: 140208 Current children cumulated CPU time (s) 827.4 Current children cumulated vsize (Kb) 142332 [startup+840.082 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 32902 0 0 0 83512 227 0 0 25 0 1 0 1855007613 143876096 32526 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 35126 32526 145 145 0 34981 0 [pid=26660] vsize: 140504 Current children cumulated CPU time (s) 837.39 Current children cumulated vsize (Kb) 142628 [startup+850.082 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 33053 0 0 0 84509 228 0 0 25 0 1 0 1855007613 144482304 32677 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 35274 32677 145 145 0 35129 0 [pid=26660] vsize: 141096 Current children cumulated CPU time (s) 847.37 Current children cumulated vsize (Kb) 143220 [startup+860.083 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 33313 0 0 0 85505 230 0 0 25 0 1 0 1855007613 145534976 32937 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 35531 32937 145 145 0 35386 0 [pid=26660] vsize: 142124 Current children cumulated CPU time (s) 857.35 Current children cumulated vsize (Kb) 144248 [startup+870.083 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 33588 0 0 0 86500 231 0 0 25 0 1 0 1855007613 146640896 33212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 35801 33212 145 145 0 35656 0 [pid=26660] vsize: 143204 Current children cumulated CPU time (s) 867.31 Current children cumulated vsize (Kb) 145328 [startup+880.083 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 33847 0 0 0 87495 233 0 0 25 0 1 0 1855007613 147677184 33471 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 36054 33471 145 145 0 35909 0 [pid=26660] vsize: 144216 Current children cumulated CPU time (s) 877.28 Current children cumulated vsize (Kb) 146340 [startup+890.084 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 34216 0 0 0 88490 236 0 0 25 0 1 0 1855007613 149172224 33840 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 36419 33840 145 145 0 36274 0 [pid=26660] vsize: 145676 Current children cumulated CPU time (s) 887.26 Current children cumulated vsize (Kb) 147800 [startup+900.084 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 34499 0 0 0 89485 238 0 0 25 0 1 0 1855007613 150310912 34123 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 36697 34123 145 145 0 36552 0 [pid=26660] vsize: 146788 Current children cumulated CPU time (s) 897.23 Current children cumulated vsize (Kb) 148912 [startup+910.086 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 34799 0 0 0 90481 241 0 0 25 0 1 0 1855007613 151543808 34423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 36998 34423 145 145 0 36853 0 [pid=26660] vsize: 147992 Current children cumulated CPU time (s) 907.22 Current children cumulated vsize (Kb) 150116 [startup+920.086 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35068 0 0 0 91475 244 0 0 25 0 1 0 1855007613 152616960 34692 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 37260 34692 145 145 0 37115 0 [pid=26660] vsize: 149040 Current children cumulated CPU time (s) 917.19 Current children cumulated vsize (Kb) 151164 [startup+930.087 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35330 0 0 0 92470 246 0 0 25 0 1 0 1855007613 153657344 34954 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 37514 34954 145 145 0 37369 0 [pid=26660] vsize: 150056 Current children cumulated CPU time (s) 927.16 Current children cumulated vsize (Kb) 152180 [startup+940.088 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35577 0 0 0 93467 247 0 0 25 0 1 0 1855007613 154669056 35201 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 37761 35201 145 145 0 37616 0 [pid=26660] vsize: 151044 Current children cumulated CPU time (s) 937.14 Current children cumulated vsize (Kb) 153168 [startup+950.088 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35785 0 0 0 94464 249 0 0 25 0 1 0 1855007613 155508736 35409 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 37966 35409 145 145 0 37821 0 [pid=26660] vsize: 151864 Current children cumulated CPU time (s) 947.13 Current children cumulated vsize (Kb) 153988 [startup+960.09 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35974 0 0 0 95460 250 0 0 25 0 1 0 1855007613 156278784 35598 4294967295 134512640 135094434 3221224432 3221223024 134556969 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 38154 35598 145 145 0 38009 0 [pid=26660] vsize: 152616 Current children cumulated CPU time (s) 957.1 Current children cumulated vsize (Kb) 154740 [startup+970.09 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36164 0 0 0 96456 252 0 0 25 0 1 0 1855007613 157032448 35788 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 38338 35788 145 145 0 38193 0 [pid=26660] vsize: 153352 Current children cumulated CPU time (s) 967.08 Current children cumulated vsize (Kb) 155476 [startup+980.091 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36334 0 0 0 97453 254 0 0 25 0 1 0 1855007613 157732864 35958 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 38509 35958 145 145 0 38364 0 [pid=26660] vsize: 154036 Current children cumulated CPU time (s) 977.07 Current children cumulated vsize (Kb) 156160 [startup+990.093 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36507 0 0 0 98450 256 0 0 25 0 1 0 1855007613 158416896 36131 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 38676 36131 145 145 0 38531 0 [pid=26660] vsize: 154704 Current children cumulated CPU time (s) 987.06 Current children cumulated vsize (Kb) 156828 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36678 0 0 0 99447 257 0 0 25 0 1 0 1855007613 159105024 36302 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 38844 36302 145 145 0 38699 0 [pid=26660] vsize: 155376 Current children cumulated CPU time (s) 997.04 Current children cumulated vsize (Kb) 157500 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36825 0 0 0 100445 259 0 0 25 0 1 0 1855007613 159690752 36449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 38987 36449 145 145 0 38842 0 [pid=26660] vsize: 155948 Current children cumulated CPU time (s) 1007.04 Current children cumulated vsize (Kb) 158072 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36984 0 0 0 101441 260 0 0 25 0 1 0 1855007613 160325632 36608 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 39142 36608 145 145 0 38997 0 [pid=26660] vsize: 156568 Current children cumulated CPU time (s) 1017.01 Current children cumulated vsize (Kb) 158692 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37129 0 0 0 102439 261 0 0 25 0 1 0 1855007613 160935936 36753 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 39291 36753 145 145 0 39146 0 [pid=26660] vsize: 157164 Current children cumulated CPU time (s) 1027 Current children cumulated vsize (Kb) 159288 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37266 0 0 0 103437 262 0 0 25 0 1 0 1855007613 161546240 36890 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 39440 36890 145 145 0 39295 0 [pid=26660] vsize: 157760 Current children cumulated CPU time (s) 1036.99 Current children cumulated vsize (Kb) 159884 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37364 0 0 0 104436 263 0 0 25 0 1 0 1855007613 161943552 36988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 39537 36988 145 145 0 39392 0 [pid=26660] vsize: 158148 Current children cumulated CPU time (s) 1046.99 Current children cumulated vsize (Kb) 160272 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37449 0 0 0 105434 264 0 0 25 0 1 0 1855007613 162287616 37073 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26660/statm): 39621 37073 145 145 0 39476 0 [pid=26660] vsize: 158484 Current children cumulated CPU time (s) 1056.98 Current children cumulated vsize (Kb) 160608 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37509 0 0 0 106433 264 0 0 25 0 1 0 1855007613 162521088 37133 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 39678 37133 145 145 0 39533 0 [pid=26660] vsize: 158712 Current children cumulated CPU time (s) 1066.97 Current children cumulated vsize (Kb) 160836 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37702 0 0 0 107429 267 0 0 25 0 1 0 1855007613 163303424 37326 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 39869 37326 145 145 0 39724 0 [pid=26660] vsize: 159476 Current children cumulated CPU time (s) 1076.96 Current children cumulated vsize (Kb) 161600 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37837 0 0 0 108427 268 0 0 25 0 1 0 1855007613 163852288 37461 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 40003 37461 145 145 0 39858 0 [pid=26660] vsize: 160012 Current children cumulated CPU time (s) 1086.95 Current children cumulated vsize (Kb) 162136 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 38152 0 0 0 109421 270 0 0 25 0 1 0 1855007613 165130240 37776 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 40315 37776 145 145 0 40170 0 [pid=26660] vsize: 161260 Current children cumulated CPU time (s) 1096.91 Current children cumulated vsize (Kb) 163384 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 38369 0 0 0 110417 272 0 0 25 0 1 0 1855007613 166006784 37993 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 40529 37993 145 145 0 40384 0 [pid=26660] vsize: 162116 Current children cumulated CPU time (s) 1106.89 Current children cumulated vsize (Kb) 164240 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 38523 0 0 0 111414 273 0 0 25 0 1 0 1855007613 166629376 38147 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 40681 38147 145 145 0 40536 0 [pid=26660] vsize: 162724 Current children cumulated CPU time (s) 1116.87 Current children cumulated vsize (Kb) 164848 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 38933 0 0 0 112407 276 0 0 25 0 1 0 1855007613 168284160 38557 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 41085 38557 145 145 0 40940 0 [pid=26660] vsize: 164340 Current children cumulated CPU time (s) 1126.83 Current children cumulated vsize (Kb) 166464 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 39220 0 0 0 113403 278 0 0 25 0 1 0 1855007613 169443328 38844 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 41368 38844 145 145 0 41223 0 [pid=26660] vsize: 165472 Current children cumulated CPU time (s) 1136.81 Current children cumulated vsize (Kb) 167596 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 39841 0 0 0 114394 282 0 0 25 0 1 0 1855007613 171954176 39465 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 41981 39465 145 145 0 41836 0 [pid=26660] vsize: 167924 Current children cumulated CPU time (s) 1146.76 Current children cumulated vsize (Kb) 170048 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 40208 0 0 0 115387 284 0 0 25 0 1 0 1855007613 173441024 39832 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 42344 39832 145 145 0 42199 0 [pid=26660] vsize: 169376 Current children cumulated CPU time (s) 1156.71 Current children cumulated vsize (Kb) 171500 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 40474 0 0 0 116382 287 0 0 25 0 1 0 1855007613 174514176 40098 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 42606 40098 145 145 0 42461 0 [pid=26660] vsize: 170424 Current children cumulated CPU time (s) 1166.69 Current children cumulated vsize (Kb) 172548 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 40750 0 0 0 117377 290 0 0 25 0 1 0 1855007613 175624192 40374 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 42877 40374 145 145 0 42732 0 [pid=26660] vsize: 171508 Current children cumulated CPU time (s) 1176.67 Current children cumulated vsize (Kb) 173632 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 41102 0 0 0 118370 292 0 0 25 0 1 0 1855007613 177053696 40726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 43226 40726 145 145 0 43081 0 [pid=26660] vsize: 172904 Current children cumulated CPU time (s) 1186.62 Current children cumulated vsize (Kb) 175028 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 41378 0 0 0 119366 294 0 0 25 0 1 0 1855007613 178167808 41002 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 43498 41002 145 145 0 43353 0 [pid=26660] vsize: 173992 Current children cumulated CPU time (s) 1196.6 Current children cumulated vsize (Kb) 176116 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 41745 0 0 0 120359 297 0 0 25 0 1 0 1855007613 179646464 41369 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 43859 41369 145 145 0 43714 0 [pid=26660] vsize: 175436 Current children cumulated CPU time (s) 1206.56 Current children cumulated vsize (Kb) 177560 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26660 Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26656/statm): 531 226 485 147 0 384 0 [pid=26656] vsize: 2124 Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 41745 0 0 0 120359 297 0 0 25 0 1 0 1855007613 179646464 41369 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26660/statm): 43859 41369 145 145 0 43714 0 [pid=26660] vsize: 175436 Current children cumulated CPU time (s) 1206.56 Current children cumulated vsize (Kb) 177560 Sending SIGTERM to -26656 Sleeping 2 seconds One traced child (pid=26656) ended because it received signal 15 (SIGTERM) One traced child (pid=26660) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.19 CPU time (s): 1206.65 CPU user time (s): 1203.59 CPU system time (s): 3.05154 CPU usage (%): 99.7072 Max. virtual memory (cumulated for all children) (Kb): 177560
ERROR: no interpretation found !