Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-scorpion.opb |
MD5SUM | 407688f2ee1c26681a4ae06671027d6f |
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 | 5640 |
Biggest coefficient in the objective function | 10536091648 |
Number of bits for the biggest coefficient in the objective function | 34 |
Sum of the numbers in the objective function | 589543467975 |
Number of bits of the sum of numbers in the objective function | 40 |
Biggest number in a constraint | 32768000000 |
Number of bits of the biggest number in a constraint | 35 |
Biggest sum of numbers in a constraint | 589543467975 |
Number of bits of the biggest sum of numbers | 40 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 7160 |
Total number of constraints | 388 |
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 | 388 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 400 |
LAUNCH ON wulflinc10 THE 2005-09-20 02:53:07 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3189 boxname=wulflinc10 idbench=845 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 407688f2ee1c26681a4ae06671027d6f /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-scorpion.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-scorpion.opb IDLAUNCH: 3189 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 786112 kB Buffers: 38420 kB Cached: 182420 kB SwapCached: 228 kB Active: 84220 kB Inactive: 139572 kB HighTotal: 131008 kB HighFree: 6748 kB LowTotal: 903652 kB LowFree: 779364 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6272 kB Slab: 19124 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:13:17 (client local time) WITH STATUS 0 IN 1207.31 SECONDS stats: 3189 7 1207.31 0
c Parsing PB file... c Converting 562 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################# c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssss c ---[ 596]---> Sorter-cost: 6011 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 594]---> Sorter-cost: 6011 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 592]---> Sorter-cost: 6011 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 590]---> Sorter-cost: 6011 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 588]---> Sorter-cost: 6011 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 586]---> Sorter-cost: 6011 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 584]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 582]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 580]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 578]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 576]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 574]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 572]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7 c ---[ 570]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7 c ---[ 568]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7 c ---[ 566]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7 c ---[ 564]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7 c ---[ 562]---> Sorter-cost: 5993 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7 c ---[ 560]---> Sorter-cost: 6087 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 558]---> Sorter-cost: 6087 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 556]---> Sorter-cost: 6087 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 554]---> Sorter-cost: 6087 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 552]---> Sorter-cost: 6087 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 550]---> Sorter-cost: 6087 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 548]---> Sorter-cost: 6326 Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 546]---> Sorter-cost: 6326 Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 544]---> Sorter-cost: 6326 Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 542]---> Sorter-cost: 6326 Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 540]---> Sorter-cost: 6326 Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 538]---> Sorter-cost: 6326 Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 536]---> Sorter-cost: 6374 Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 534]---> Sorter-cost: 6374 Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 532]---> Sorter-cost: 6374 Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 530]---> Sorter-cost: 6374 Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 528]---> Sorter-cost: 6374 Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 526]---> Sorter-cost: 6374 Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 524]---> Sorter-cost: 3933 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2 c ---[ 522]---> Sorter-cost: 3933 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2 c ---[ 520]---> Sorter-cost: 3933 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2 c ---[ 518]---> Sorter-cost: 3933 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2 c ---[ 516]---> Sorter-cost: 3933 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2 c ---[ 514]---> Sorter-cost: 3933 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2 c ---[ 512]---> Adder-cost: 636 maxlim: 314572500 bits: 29/29 c ---[ 510]---> Adder-cost: 636 maxlim: 314572500 bits: 29/29 c ---[ 508]---> Adder-cost: 636 maxlim: 314572500 bits: 29/29 c ---[ 506]---> Adder-cost: 636 maxlim: 314572500 bits: 29/29 c ---[ 504]---> Adder-cost: 636 maxlim: 314572500 bits: 29/29 c ---[ 502]---> Adder-cost: 636 maxlim: 314572500 bits: 29/29 c ---[ 500]---> Sorter-cost: 1658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 498]---> Sorter-cost: 1658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 496]---> Sorter-cost: 1658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 494]---> Sorter-cost: 1658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 492]---> Sorter-cost: 1658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 490]---> Sorter-cost: 1658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 488]---> Sorter-cost: 1439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 486]---> Sorter-cost: 1439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> Sorter-cost: 1439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 482]---> Sorter-cost: 1439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 480]---> Sorter-cost: 1439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 478]---> Sorter-cost: 1439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 476]---> BDD-cost: 58 c ---[ 474]---> BDD-cost: 58 c ---[ 472]---> BDD-cost: 58 c ---[ 470]---> BDD-cost: 58 c ---[ 468]---> BDD-cost: 58 c ---[ 466]---> BDD-cost: 58 c ---[ 464]---> BDD-cost: 172 c ---[ 462]---> BDD-cost: 172 c ---[ 460]---> BDD-cost: 172 c ---[ 458]---> BDD-cost: 172 c ---[ 456]---> BDD-cost: 172 c ---[ 454]---> BDD-cost: 172 c ---[ 452]---> Sorter-cost: 760 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 450]---> Sorter-cost: 760 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 448]---> Sorter-cost: 760 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 446]---> Sorter-cost: 760 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 444]---> Sorter-cost: 760 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 442]---> Sorter-cost: 760 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 440]---> BDD-cost: 172 c ---[ 438]---> BDD-cost: 172 c ---[ 436]---> BDD-cost: 172 c ---[ 434]---> BDD-cost: 172 c ---[ 432]---> BDD-cost: 172 c ---[ 430]---> BDD-cost: 172 c ---[ 428]---> BDD-cost: 58 c ---[ 426]---> BDD-cost: 58 c ---[ 424]---> BDD-cost: 58 c ---[ 422]---> BDD-cost: 58 c ---[ 420]---> BDD-cost: 58 c ---[ 418]---> BDD-cost: 58 c ---[ 416]---> BDD-cost: 58 c ---[ 414]---> BDD-cost: 58 c ---[ 412]---> BDD-cost: 58 c ---[ 410]---> BDD-cost: 58 c ---[ 408]---> BDD-cost: 58 c ---[ 406]---> BDD-cost: 58 c ---[ 404]---> BDD-cost: 58 c ---[ 402]---> BDD-cost: 58 c ---[ 400]---> BDD-cost: 58 c ---[ 398]---> BDD-cost: 58 c ---[ 396]---> BDD-cost: 58 c ---[ 394]---> BDD-cost: 58 c ---[ 392]---> BDD-cost: 58 c ---[ 390]---> BDD-cost: 58 c ---[ 388]---> BDD-cost: 58 c ---[ 386]---> BDD-cost: 58 c ---[ 384]---> BDD-cost: 58 c ---[ 382]---> BDD-cost: 58 c ---[ 381]---> Sorter-cost: 3271 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 c ---[ 380]---> Adder-cost: 440 maxlim: 62911338 bits: 27/26 c ---[ 379]---> Adder-cost: 440 maxlim: 62912311 bits: 27/26 c ---[ 378]---> Adder-cost: 671 maxlim: 62914499 bits: 27/26 c ---[ 377]---> Adder-cost: 440 maxlim: 62914499 bits: 27/26 c ---[ 376]---> Sorter-cost: 3271 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 c ---[ 375]---> Sorter-cost: 725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 374]---> Sorter-cost: 727 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 373]---> Sorter-cost: 1550 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 372]---> Sorter-cost: 1554 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 371]---> Sorter-cost: 2469 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 370]---> Sorter-cost: 2475 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 369]---> Sorter-cost: 3828 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 368]---> Sorter-cost: 3832 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 367]---> Sorter-cost: 1550 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 366]---> Sorter-cost: 1552 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 365]---> Sorter-cost: 1420 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 c ---[ 364]---> Sorter-cost: 1420 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 c ---[ 363]---> Sorter-cost: 2040 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[ 362]---> Sorter-cost: 3946 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 7 c ---[ 361]---> Adder-cost: 467 maxlim: 933882 bits: 21/20 c ---[ 360]---> Adder-cost: 559 maxlim: 933882 bits: 21/20 c ---[ 359]---> Adder-cost: 649 maxlim: 933882 bits: 21/20 c ---[ 358]---> Sorter-cost: 3946 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 7 c ---[ 357]---> Adder-cost: 436 maxlim: 9469674 bits: 24/24 c ---[ 356]---> Adder-cost: 476 maxlim: 9469700 bits: 25/24 c ---[ 355]---> Adder-cost: 516 maxlim: 9469741 bits: 25/24 c ---[ 354]---> Adder-cost: 556 maxlim: 9469838 bits: 25/24 c ---[ 353]---> Adder-cost: 556 maxlim: 9469940 bits: 25/24 c ---[ 352]---> Adder-cost: 476 maxlim: 9469940 bits: 25/24 c ---[ 344]---> Sorter-cost: 1416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 342]---> Sorter-cost: 1416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 340]---> Sorter-cost: 1416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 338]---> Sorter-cost: 1416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 336]---> Sorter-cost: 1416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 334]---> Sorter-cost: 1416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 332]---> Sorter-cost: 4634 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 330]---> Sorter-cost: 4634 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 328]---> Sorter-cost: 4634 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 326]---> Sorter-cost: 4634 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 324]---> Sorter-cost: 4634 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 322]---> Sorter-cost: 4634 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 320]---> Sorter-cost: 722 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 318]---> Sorter-cost: 722 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 316]---> Sorter-cost: 722 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 314]---> Sorter-cost: 722 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 312]---> Sorter-cost: 722 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 310]---> Sorter-cost: 722 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 308]---> Sorter-cost: 4594 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 306]---> Sorter-cost: 4594 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 304]---> Sorter-cost: 4594 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 302]---> Sorter-cost: 4594 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 300]---> Sorter-cost: 4594 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 298]---> Sorter-cost: 4594 Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 296]---> Adder-cost: 504 maxlim: 64551975 bits: 27/26 c ---[ 294]---> Adder-cost: 504 maxlim: 64551975 bits: 27/26 c ---[ 292]---> Adder-cost: 504 maxlim: 64551975 bits: 27/26 c ---[ 290]---> Adder-cost: 504 maxlim: 64551975 bits: 27/26 c ---[ 288]---> Adder-cost: 504 maxlim: 64551975 bits: 27/26 c ---[ 286]---> Adder-cost: 504 maxlim: 64551975 bits: 27/26 c ---[ 284]---> Adder-cost: 384 maxlim: 13631475 bits: 25/24 c ---[ 282]---> Adder-cost: 384 maxlim: 13631475 bits: 25/24 c ---[ 280]---> Adder-cost: 384 maxlim: 13631475 bits: 25/24 c ---[ 278]---> Adder-cost: 384 maxlim: 13631475 bits: 25/24 c ---[ 276]---> Adder-cost: 384 maxlim: 13631475 bits: 25/24 c ---[ 274]---> Adder-cost: 384 maxlim: 13631475 bits: 25/24 c ---[ 272]---> Sorter-cost: 4081 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[ 270]---> Sorter-cost: 4081 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[ 268]---> Sorter-cost: 4081 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[ 266]---> Sorter-cost: 4081 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[ 264]---> Sorter-cost: 4081 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[ 262]---> Sorter-cost: 4081 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[ 260]---> Adder-cost: 507 maxlim: 28311525 bits: 26/25 c ---[ 258]---> Adder-cost: 507 maxlim: 28311525 bits: 26/25 c ---[ 256]---> Adder-cost: 507 maxlim: 28311525 bits: 26/25 c ---[ 254]---> Adder-cost: 507 maxlim: 28311525 bits: 26/25 c ---[ 252]---> Adder-cost: 507 maxlim: 28311525 bits: 26/25 c ---[ 250]---> Adder-cost: 507 maxlim: 28311525 bits: 26/25 c ---[ 248]---> Sorter-cost: 1525 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 246]---> Sorter-cost: 1525 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 244]---> Sorter-cost: 1525 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 242]---> Sorter-cost: 1525 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 240]---> Sorter-cost: 1525 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 238]---> Sorter-cost: 1525 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 236]---> Sorter-cost: 3931 Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 234]---> Sorter-cost: 3931 Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 232]---> Sorter-cost: 3931 Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 230]---> Sorter-cost: 3931 Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 228]---> Sorter-cost: 3931 Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 226]---> Sorter-cost: 3931 Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 224]---> Sorter-cost: 2881 Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 222]---> Sorter-cost: 2881 Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 220]---> Sorter-cost: 2881 Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 218]---> Sorter-cost: 2881 Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 216]---> Sorter-cost: 2881 Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 214]---> Sorter-cost: 2881 Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 212]---> Sorter-cost: 3524 Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 210]---> Sorter-cost: 3524 Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 208]---> Sorter-cost: 3524 Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 206]---> Sorter-cost: 3524 Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 204]---> Sorter-cost: 3524 Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 202]---> Sorter-cost: 3524 Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 200]---> Adder-cost: 656 maxlim: 160431975 bits: 29/28 c ---[ 198]---> Adder-cost: 660 maxlim: 160431975 bits: 29/28 c ---[ 196]---> Adder-cost: 660 maxlim: 160431975 bits: 29/28 c ---[ 194]---> Adder-cost: 660 maxlim: 160431975 bits: 29/28 c ---[ 192]---> Adder-cost: 660 maxlim: 160431975 bits: 29/28 c ---[ 190]---> Adder-cost: 660 maxlim: 160431975 bits: 29/28 c ---[ 188]---> Sorter-cost: 3131 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[ 186]---> Sorter-cost: 3131 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[ 184]---> Sorter-cost: 3131 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[ 182]---> Sorter-cost: 3131 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[ 180]---> Sorter-cost: 3131 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[ 178]---> Sorter-cost: 3131 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[ 176]---> Adder-cost: 460 maxlim: 28311525 bits: 26/25 c ---[ 174]---> Adder-cost: 460 maxlim: 28311525 bits: 26/25 c ---[ 172]---> Adder-cost: 460 maxlim: 28311525 bits: 26/25 c ---[ 170]---> Adder-cost: 460 maxlim: 28311525 bits: 26/25 c ---[ 168]---> Adder-cost: 460 maxlim: 28311525 bits: 26/25 c ---[ 166]---> Adder-cost: 460 maxlim: 28311525 bits: 26/25 c ---[ 164]---> Sorter-cost: 1143 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 1143 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 1143 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 1143 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 1143 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 154]---> Sorter-cost: 1143 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 152]---> Sorter-cost: 1173 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 150]---> Sorter-cost: 1173 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 148]---> Sorter-cost: 1173 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 146]---> Sorter-cost: 1173 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 144]---> Sorter-cost: 1173 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 142]---> Sorter-cost: 1173 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 140]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 138]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 136]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 134]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 132]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 130]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 c ---[ 79]---> BDD-cost: 58 c ---[ 77]---> BDD-cost: 58 c ---[ 75]---> BDD-cost: 58 c ---[ 73]---> BDD-cost: 58 c ---[ 71]---> BDD-cost: 58 c ---[ 69]---> BDD-cost: 58 c ---[ 67]---> BDD-cost: 58 c ---[ 65]---> BDD-cost: 58 c ---[ 63]---> BDD-cost: 58 c ---[ 61]---> BDD-cost: 58 c ---[ 59]---> BDD-cost: 58 c ---[ 57]---> BDD-cost: 58 c ---[ 55]---> BDD-cost: 58 c ---[ 53]---> BDD-cost: 58 c ---[ 51]---> BDD-cost: 58 c ---[ 49]---> BDD-cost: 58 c ---[ 47]---> BDD-cost: 58 c ---[ 45]---> BDD-cost: 58 c ---[ 43]---> BDD-cost: 172 c ---[ 41]---> BDD-cost: 58 c ---[ 39]---> BDD-cost: 58 c ---[ 38]---> BDD-cost: 3 c ---[ 37]---> BDD-cost: 4 c ---[ 36]---> BDD-cost: 3 c ---[ 35]---> BDD-cost: 4 c ---[ 34]---> BDD-cost: 5 c ---[ 33]---> BDD-cost: 6 c ---[ 32]---> BDD-cost: 6 c ---[ 31]---> BDD-cost: 4 c ---[ 30]---> BDD-cost: 4 c ---[ 29]---> BDD-cost: 5 c ---[ 28]---> BDD-cost: 5 c ---[ 27]---> BDD-cost: 7 c ---[ 26]---> BDD-cost: 7 c ---[ 25]---> BDD-cost: 5 c ---[ 24]---> BDD-cost: 5 c ---[ 23]---> BDD-cost: 4 c ---[ 22]---> BDD-cost: 6 c ---[ 21]---> BDD-cost: 4 c ---[ 20]---> BDD-cost: 4 c ---[ 19]---> BDD-cost: 4 c ---[ 18]---> BDD-cost: 2 c ---[ 17]---> BDD-cost: 2 c ---[ 16]---> BDD-cost: 3 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 4 c ---[ 13]---> BDD-cost: 3 c ---[ 12]---> BDD-cost: 2 c ---[ 11]---> BDD-cost: 3 c ---[ 10]---> BDD-cost: 4 c ---[ 9]---> BDD-cost: 3 c ---[ 8]---> BDD-cost: 5 c ---[ 7]---> BDD-cost: 2 c ---[ 6]---> BDD-cost: 4 c ---[ 5]---> BDD-cost: 4 c ---[ 4]---> BDD-cost: 4 c ---[ 3]---> BDD-cost: 5 c ---[ 2]---> BDD-cost: 3 c ---[ 1]---> BDD-cost: 2 c ---[ 0]---> BDD-cost: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1487022 3712364 | 495674 0 0 nan | 0.000 % | c | 105 | 1486988 3712291 | 545241 97 1917 19.8 | 3.939 % | c | 257 | 1486988 3712291 | 599765 249 6540 26.3 | 3.939 % | c | 482 | 1486988 3712291 | 659742 474 11053 23.3 | 3.939 % | c | 819 | 1486963 3712234 | 725716 810 20009 24.7 | 3.941 % | c | 1326 | 1486742 3711734 | 798287 1304 27952 21.4 | 3.953 % | c | 2086 | 1486706 3711655 | 878116 2061 43612 21.2 | 3.956 % | c | 3225 | 1485882 3709781 | 965928 3159 65814 20.8 | 4.003 % | c | 4933 | 1485788 3709572 | 1062521 4856 108654 22.4 | 4.009 % | c | 7499 | 1485674 3709316 | 1168773 7412 193875 26.2 | 4.015 % | c | 11343 | 1485367 3708618 | 1285650 11237 386372 34.4 | 4.032 % | c | 17109 | 1484307 3706149 | 1414215 16930 572771 33.8 | 4.087 % | c | 25758 | 1479304 3694129 | 1555637 25380 896632 35.3 | 4.346 % | c | 38732 | 1457528 3642805 | 1711201 37975 1371377 36.1 | 5.682 % | c | 58193 | 1424492 3564636 | 1882321 56635 2139712 37.8 | 7.953 % | c | 87385 | 1396504 3492008 | 2070553 76191 3037307 39.9 | 9.542 % | c | 131175 | 1375745 3438759 | 2277608 114021 5134768 45.0 | 10.814 % | c | 196859 | 1370848 3427268 | 2505369 179162 8654298 48.3 | 11.084 % |
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/13906/stat): 13906 (minisat+_script) R 13905 13906 22582 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796895075 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/13906/statm): 174 3 169 147 0 27 0 [pid=13906] 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=13907 New process pid=13908 New process pid=13909 execve syscall for /bin/sed executable One traced child (pid=13908) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=13909) exited with status: 0 One traced child (pid=13907) exited with status: 0 New process pid=13910 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-scorpion.opb [startup+10.0052 s] Raw data (loadavg): 0.77 0.91 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 1679 0 0 0 983 6 0 0 25 0 1 0 1796895080 6615040 1499 4294967295 134512640 135094434 3221224432 3221222336 134600310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 1615 1499 145 145 0 1470 0 [pid=13910] vsize: 6460 Current children cumulated CPU time (s) 9.9 Current children cumulated vsize (Kb) 8584 [startup+20.0058 s] Raw data (loadavg): 0.80 0.92 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 2591 0 0 0 1980 9 0 0 25 0 1 0 1796895080 11165696 2246 4294967295 134512640 135094434 3221224432 3221220928 134600314 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 2726 2246 145 145 0 2581 0 [pid=13910] vsize: 10904 Current children cumulated CPU time (s) 19.9 Current children cumulated vsize (Kb) 13028 [startup+30.0063 s] Raw data (loadavg): 0.83 0.92 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 3596 0 0 0 2976 12 0 0 25 0 1 0 1796895080 13479936 2921 4294967295 134512640 135094434 3221224432 3221221632 134600314 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 3291 2921 145 145 0 3146 0 [pid=13910] vsize: 13164 Current children cumulated CPU time (s) 29.89 Current children cumulated vsize (Kb) 15288 [startup+40.0079 s] Raw data (loadavg): 0.86 0.92 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 3928 0 0 0 3975 13 0 0 25 0 1 0 1796895080 14016512 3127 4294967295 134512640 135094434 3221224432 3221222192 134783048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 3422 3127 145 145 0 3277 0 [pid=13910] vsize: 13688 Current children cumulated CPU time (s) 39.89 Current children cumulated vsize (Kb) 15812 [startup+50.0084 s] Raw data (loadavg): 0.88 0.92 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 4321 0 0 0 4973 14 0 0 25 0 1 0 1796895080 14622720 3394 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 3570 3394 145 145 0 3425 0 [pid=13910] vsize: 14280 Current children cumulated CPU time (s) 49.88 Current children cumulated vsize (Kb) 16404 [startup+60.01 s] Raw data (loadavg): 0.90 0.92 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 6708 0 0 0 5963 21 0 0 25 0 1 0 1796895080 22757376 4927 4294967295 134512640 135094434 3221224432 3221220204 134676240 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 5556 4927 145 145 0 5411 0 [pid=13910] vsize: 22224 Current children cumulated CPU time (s) 59.85 Current children cumulated vsize (Kb) 24348 [startup+70.0115 s] Raw data (loadavg): 0.91 0.93 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 7359 0 0 0 6960 23 0 0 25 0 1 0 1796895080 24031232 5421 4294967295 134512640 135094434 3221224432 3221221552 134676308 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 5867 5421 145 145 0 5722 0 [pid=13910] vsize: 23468 Current children cumulated CPU time (s) 69.84 Current children cumulated vsize (Kb) 25592 [startup+80.0121 s] Raw data (loadavg): 0.92 0.93 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 7764 0 0 0 7957 24 0 0 25 0 1 0 1796895080 24997888 5787 4294967295 134512640 135094434 3221224432 3221221376 134677049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 6103 5787 145 145 0 5958 0 [pid=13910] vsize: 24412 Current children cumulated CPU time (s) 79.82 Current children cumulated vsize (Kb) 26536 [startup+90.0127 s] Raw data (loadavg): 0.94 0.93 0.90 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 8325 0 0 0 8954 26 0 0 25 0 1 0 1796895080 26361856 6312 4294967295 134512640 135094434 3221224432 3221220608 134780812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 6436 6312 145 145 0 6291 0 [pid=13910] vsize: 25744 Current children cumulated CPU time (s) 89.81 Current children cumulated vsize (Kb) 27868 [startup+100.013 s] Raw data (loadavg): 0.95 0.93 0.91 1/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) T 13906 13906 22582 0 -1 0 11667 0 0 0 9933 38 0 0 24 0 1 0 1796895080 47321088 9517 4294967295 134512640 135094434 3221224432 3221169564 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13910/statm): 11553 9517 145 145 0 11408 0 [pid=13910] vsize: 46212 Current children cumulated CPU time (s) 99.72 Current children cumulated vsize (Kb) 48336 [startup+110.015 s] Raw data (loadavg): 0.95 0.93 0.91 1/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) T 13906 13906 22582 0 -1 0 40789 0 0 0 10679 157 0 0 22 0 1 0 1796895080 174149632 38639 4294967295 134512640 135094434 3221224432 3221184060 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13910/statm): 42517 38639 145 145 0 42372 0 [pid=13910] vsize: 170068 Current children cumulated CPU time (s) 108.37 Current children cumulated vsize (Kb) 172192 [startup+120.015 s] Raw data (loadavg): 0.96 0.94 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 41721 0 0 0 11670 161 0 0 25 0 1 0 1796895080 176873472 39571 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 43182 39571 145 145 0 43037 0 [pid=13910] vsize: 172728 Current children cumulated CPU time (s) 118.32 Current children cumulated vsize (Kb) 174852 [startup+130.016 s] Raw data (loadavg): 0.97 0.94 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 41777 0 0 0 12669 162 0 0 25 0 1 0 1796895080 177102848 39627 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 43238 39627 145 145 0 43093 0 [pid=13910] vsize: 172952 Current children cumulated CPU time (s) 128.32 Current children cumulated vsize (Kb) 175076 [startup+140.016 s] Raw data (loadavg): 0.97 0.94 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 41924 0 0 0 13667 163 0 0 25 0 1 0 1796895080 177709056 39774 4294967295 134512640 135094434 3221224432 3221223104 134553437 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 43386 39774 145 145 0 43241 0 [pid=13910] vsize: 173544 Current children cumulated CPU time (s) 138.31 Current children cumulated vsize (Kb) 175668 [startup+150.017 s] Raw data (loadavg): 0.97 0.94 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42122 0 0 0 14663 165 0 0 25 0 1 0 1796895080 178536448 39972 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 43588 39972 145 145 0 43443 0 [pid=13910] vsize: 174352 Current children cumulated CPU time (s) 148.29 Current children cumulated vsize (Kb) 176476 [startup+160.019 s] Raw data (loadavg): 0.98 0.94 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42238 0 0 0 15660 167 0 0 25 0 1 0 1796895080 179007488 40088 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 43703 40088 145 145 0 43558 0 [pid=13910] vsize: 174812 Current children cumulated CPU time (s) 158.28 Current children cumulated vsize (Kb) 176936 [startup+170.019 s] Raw data (loadavg): 0.98 0.94 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) T 13906 13906 22582 0 -1 0 42365 0 0 0 16659 168 0 0 25 0 1 0 1796895080 179580928 40215 4294967295 134512640 135094434 3221224432 3221223128 134801757 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13910/statm): 43843 40215 145 145 0 43698 0 [pid=13910] vsize: 175372 Current children cumulated CPU time (s) 168.28 Current children cumulated vsize (Kb) 177496 [startup+180.02 s] Raw data (loadavg): 0.98 0.94 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42423 0 0 0 17658 168 0 0 25 0 1 0 1796895080 179810304 40273 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 43899 40273 145 145 0 43754 0 [pid=13910] vsize: 175596 Current children cumulated CPU time (s) 178.27 Current children cumulated vsize (Kb) 177720 [startup+190.02 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42601 0 0 0 18656 169 0 0 25 0 1 0 1796895080 180502528 40451 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 44068 40451 145 145 0 43923 0 [pid=13910] vsize: 176272 Current children cumulated CPU time (s) 188.26 Current children cumulated vsize (Kb) 178396 [startup+200.02 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42795 0 0 0 19652 171 0 0 25 0 1 0 1796895080 181248000 40645 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 44250 40645 145 145 0 44105 0 [pid=13910] vsize: 177000 Current children cumulated CPU time (s) 198.24 Current children cumulated vsize (Kb) 179124 [startup+210.02 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42952 0 0 0 20649 173 0 0 25 0 1 0 1796895080 181878784 40802 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 44404 40802 145 145 0 44259 0 [pid=13910] vsize: 177616 Current children cumulated CPU time (s) 208.23 Current children cumulated vsize (Kb) 179740 [startup+220.022 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42972 0 0 0 21649 173 0 0 25 0 1 0 1796895080 181952512 40822 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 44422 40822 145 145 0 44277 0 [pid=13910] vsize: 177688 Current children cumulated CPU time (s) 218.23 Current children cumulated vsize (Kb) 179812 [startup+230.022 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43102 0 0 0 22647 174 0 0 25 0 1 0 1796895080 182575104 40952 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 44574 40952 145 145 0 44429 0 [pid=13910] vsize: 178296 Current children cumulated CPU time (s) 228.22 Current children cumulated vsize (Kb) 180420 [startup+240.022 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43140 0 0 0 23646 175 0 0 25 0 1 0 1796895080 182722560 40990 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 44610 40990 145 145 0 44465 0 [pid=13910] vsize: 178440 Current children cumulated CPU time (s) 238.22 Current children cumulated vsize (Kb) 180564 [startup+250.023 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43419 0 0 0 24641 177 0 0 25 0 1 0 1796895080 183848960 41269 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 44885 41269 145 145 0 44740 0 [pid=13910] vsize: 179540 Current children cumulated CPU time (s) 248.19 Current children cumulated vsize (Kb) 181664 [startup+260.023 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43601 0 0 0 25638 178 0 0 25 0 1 0 1796895080 184578048 41451 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 45063 41451 145 145 0 44918 0 [pid=13910] vsize: 180252 Current children cumulated CPU time (s) 258.17 Current children cumulated vsize (Kb) 182376 [startup+270.024 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43637 0 0 0 26638 178 0 0 25 0 1 0 1796895080 184717312 41487 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 45097 41487 145 145 0 44952 0 [pid=13910] vsize: 180388 Current children cumulated CPU time (s) 268.17 Current children cumulated vsize (Kb) 182512 [startup+280.024 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43854 0 0 0 27635 180 0 0 25 0 1 0 1796895080 185593856 41704 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 45311 41704 145 145 0 45166 0 [pid=13910] vsize: 181244 Current children cumulated CPU time (s) 278.16 Current children cumulated vsize (Kb) 183368 [startup+290.025 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43987 0 0 0 28633 181 0 0 25 0 1 0 1796895080 186126336 41837 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 45441 41837 145 145 0 45296 0 [pid=13910] vsize: 181764 Current children cumulated CPU time (s) 288.15 Current children cumulated vsize (Kb) 183888 [startup+300.025 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44179 0 0 0 29630 182 0 0 25 0 1 0 1796895080 186896384 42029 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 45629 42029 145 145 0 45484 0 [pid=13910] vsize: 182516 Current children cumulated CPU time (s) 298.13 Current children cumulated vsize (Kb) 184640 [startup+310.027 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44354 0 0 0 30627 184 0 0 25 0 1 0 1796895080 187596800 42204 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 45800 42204 145 145 0 45655 0 [pid=13910] vsize: 183200 Current children cumulated CPU time (s) 308.12 Current children cumulated vsize (Kb) 185324 [startup+320.028 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44632 0 0 0 31621 186 0 0 25 0 1 0 1796895080 188973056 42482 4294967295 134512640 135094434 3221224432 3221223112 134551489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46136 42482 145 145 0 45991 0 [pid=13910] vsize: 184544 Current children cumulated CPU time (s) 318.08 Current children cumulated vsize (Kb) 186668 [startup+330.028 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44787 0 0 0 32618 187 0 0 25 0 1 0 1796895080 189595648 42637 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46288 42637 145 145 0 46143 0 [pid=13910] vsize: 185152 Current children cumulated CPU time (s) 328.06 Current children cumulated vsize (Kb) 187276 [startup+340.03 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44839 0 0 0 33617 188 0 0 25 0 1 0 1796895080 189800448 42689 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46338 42689 145 145 0 46193 0 [pid=13910] vsize: 185352 Current children cumulated CPU time (s) 338.06 Current children cumulated vsize (Kb) 187476 [startup+350.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44904 0 0 0 34617 188 0 0 25 0 1 0 1796895080 190062592 42754 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46402 42754 145 145 0 46257 0 [pid=13910] vsize: 185608 Current children cumulated CPU time (s) 348.06 Current children cumulated vsize (Kb) 187732 [startup+360.03 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45035 0 0 0 35614 189 0 0 25 0 1 0 1796895080 190582784 42885 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46529 42885 145 145 0 46384 0 [pid=13910] vsize: 186116 Current children cumulated CPU time (s) 358.04 Current children cumulated vsize (Kb) 188240 [startup+370.03 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45117 0 0 0 36614 189 0 0 25 0 1 0 1796895080 190914560 42967 4294967295 134512640 135094434 3221224432 3221223024 134557363 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46610 42967 145 145 0 46465 0 [pid=13910] vsize: 186440 Current children cumulated CPU time (s) 368.04 Current children cumulated vsize (Kb) 188564 [startup+380.03 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45209 0 0 0 37613 190 0 0 25 0 1 0 1796895080 191283200 43059 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46700 43059 145 145 0 46555 0 [pid=13910] vsize: 186800 Current children cumulated CPU time (s) 378.04 Current children cumulated vsize (Kb) 188924 [startup+390.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45337 0 0 0 38610 191 0 0 25 0 1 0 1796895080 191795200 43187 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46825 43187 145 145 0 46680 0 [pid=13910] vsize: 187300 Current children cumulated CPU time (s) 388.02 Current children cumulated vsize (Kb) 189424 [startup+400.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45437 0 0 0 39609 192 0 0 25 0 1 0 1796895080 192196608 43287 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 46923 43287 145 145 0 46778 0 [pid=13910] vsize: 187692 Current children cumulated CPU time (s) 398.02 Current children cumulated vsize (Kb) 189816 [startup+410.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45526 0 0 0 40608 193 0 0 25 0 1 0 1796895080 192557056 43376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47011 43376 145 145 0 46866 0 [pid=13910] vsize: 188044 Current children cumulated CPU time (s) 408.02 Current children cumulated vsize (Kb) 190168 [startup+420.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45620 0 0 0 41606 194 0 0 25 0 1 0 1796895080 192937984 43470 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47104 43470 145 145 0 46959 0 [pid=13910] vsize: 188416 Current children cumulated CPU time (s) 418.01 Current children cumulated vsize (Kb) 190540 [startup+430.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45730 0 0 0 42604 195 0 0 25 0 1 0 1796895080 193380352 43580 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47212 43580 145 145 0 47067 0 [pid=13910] vsize: 188848 Current children cumulated CPU time (s) 428 Current children cumulated vsize (Kb) 190972 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45815 0 0 0 43602 196 0 0 25 0 1 0 1796895080 193724416 43665 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47296 43665 145 145 0 47151 0 [pid=13910] vsize: 189184 Current children cumulated CPU time (s) 437.99 Current children cumulated vsize (Kb) 191308 [startup+450.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45882 0 0 0 44601 197 0 0 25 0 1 0 1796895080 193998848 43732 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47363 43732 145 145 0 47218 0 [pid=13910] vsize: 189452 Current children cumulated CPU time (s) 447.99 Current children cumulated vsize (Kb) 191576 [startup+460.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45969 0 0 0 45599 198 0 0 25 0 1 0 1796895080 194367488 43819 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47453 43819 145 145 0 47308 0 [pid=13910] vsize: 189812 Current children cumulated CPU time (s) 457.98 Current children cumulated vsize (Kb) 191936 [startup+470.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46056 0 0 0 46598 199 0 0 25 0 1 0 1796895080 194711552 43906 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47537 43906 145 145 0 47392 0 [pid=13910] vsize: 190148 Current children cumulated CPU time (s) 467.98 Current children cumulated vsize (Kb) 192272 [startup+480.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46183 0 0 0 47596 200 0 0 25 0 1 0 1796895080 195227648 44033 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47663 44033 145 145 0 47518 0 [pid=13910] vsize: 190652 Current children cumulated CPU time (s) 477.97 Current children cumulated vsize (Kb) 192776 [startup+490.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46230 0 0 0 48596 200 0 0 25 0 1 0 1796895080 195420160 44080 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47710 44080 145 145 0 47565 0 [pid=13910] vsize: 190840 Current children cumulated CPU time (s) 487.97 Current children cumulated vsize (Kb) 192964 [startup+500.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46411 0 0 0 49592 202 0 0 25 0 1 0 1796895080 196149248 44261 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47888 44261 145 145 0 47743 0 [pid=13910] vsize: 191552 Current children cumulated CPU time (s) 497.95 Current children cumulated vsize (Kb) 193676 [startup+510.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46492 0 0 0 50591 202 0 0 25 0 1 0 1796895080 196476928 44342 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 47968 44342 145 145 0 47823 0 [pid=13910] vsize: 191872 Current children cumulated CPU time (s) 507.94 Current children cumulated vsize (Kb) 193996 [startup+520.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46615 0 0 0 51590 203 0 0 25 0 1 0 1796895080 196952064 44465 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 48084 44465 145 145 0 47939 0 [pid=13910] vsize: 192336 Current children cumulated CPU time (s) 517.94 Current children cumulated vsize (Kb) 194460 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46617 0 0 0 52590 203 0 0 25 0 1 0 1796895080 196960256 44467 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 48086 44467 145 145 0 47941 0 [pid=13910] vsize: 192344 Current children cumulated CPU time (s) 527.94 Current children cumulated vsize (Kb) 194468 [startup+540.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46696 0 0 0 53589 204 0 0 25 0 1 0 1796895080 197279744 44546 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 48164 44546 145 145 0 48019 0 [pid=13910] vsize: 192656 Current children cumulated CPU time (s) 537.94 Current children cumulated vsize (Kb) 194780 [startup+550.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46776 0 0 0 54588 204 0 0 25 0 1 0 1796895080 197603328 44626 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 48243 44626 145 145 0 48098 0 [pid=13910] vsize: 192972 Current children cumulated CPU time (s) 547.93 Current children cumulated vsize (Kb) 195096 [startup+560.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46979 0 0 0 55586 205 0 0 25 0 1 0 1796895080 198402048 44829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 48438 44829 145 145 0 48293 0 [pid=13910] vsize: 193752 Current children cumulated CPU time (s) 557.92 Current children cumulated vsize (Kb) 195876 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 47436 0 0 0 56578 208 0 0 25 0 1 0 1796895080 200249344 45286 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 48889 45286 145 145 0 48744 0 [pid=13910] vsize: 195556 Current children cumulated CPU time (s) 567.87 Current children cumulated vsize (Kb) 197680 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 47639 0 0 0 57574 210 0 0 25 0 1 0 1796895080 201068544 45489 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 49089 45489 145 145 0 48944 0 [pid=13910] vsize: 196356 Current children cumulated CPU time (s) 577.85 Current children cumulated vsize (Kb) 198480 [startup+590.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 47844 0 0 0 58570 212 0 0 25 0 1 0 1796895080 201895936 45694 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 49291 45694 145 145 0 49146 0 [pid=13910] vsize: 197164 Current children cumulated CPU time (s) 587.83 Current children cumulated vsize (Kb) 199288 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 47987 0 0 0 59567 213 0 0 25 0 1 0 1796895080 202469376 45837 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 49431 45837 145 145 0 49286 0 [pid=13910] vsize: 197724 Current children cumulated CPU time (s) 597.81 Current children cumulated vsize (Kb) 199848 [startup+610.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48191 0 0 0 60565 214 0 0 25 0 1 0 1796895080 203292672 46041 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 49632 46041 145 145 0 49487 0 [pid=13910] vsize: 198528 Current children cumulated CPU time (s) 607.8 Current children cumulated vsize (Kb) 200652 [startup+620.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48445 0 0 0 61560 216 0 0 25 0 1 0 1796895080 204316672 46295 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 49882 46295 145 145 0 49737 0 [pid=13910] vsize: 199528 Current children cumulated CPU time (s) 617.77 Current children cumulated vsize (Kb) 201652 [startup+630.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48547 0 0 0 62558 217 0 0 25 0 1 0 1796895080 204726272 46397 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 49982 46397 145 145 0 49837 0 [pid=13910] vsize: 199928 Current children cumulated CPU time (s) 627.76 Current children cumulated vsize (Kb) 202052 [startup+640.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48627 0 0 0 63557 217 0 0 25 0 1 0 1796895080 205045760 46477 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 50060 46477 145 145 0 49915 0 [pid=13910] vsize: 200240 Current children cumulated CPU time (s) 637.75 Current children cumulated vsize (Kb) 202364 [startup+650.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48790 0 0 0 64555 219 0 0 25 0 1 0 1796895080 206192640 46640 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 50340 46640 145 145 0 50195 0 [pid=13910] vsize: 201360 Current children cumulated CPU time (s) 647.75 Current children cumulated vsize (Kb) 203484 [startup+660.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48952 0 0 0 65551 220 0 0 25 0 1 0 1796895080 206848000 46802 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 50500 46802 145 145 0 50355 0 [pid=13910] vsize: 202000 Current children cumulated CPU time (s) 657.72 Current children cumulated vsize (Kb) 204124 [startup+670.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49106 0 0 0 66549 221 0 0 25 0 1 0 1796895080 207470592 46956 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 50652 46956 145 145 0 50507 0 [pid=13910] vsize: 202608 Current children cumulated CPU time (s) 667.71 Current children cumulated vsize (Kb) 204732 [startup+680.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49253 0 0 0 67547 222 0 0 25 0 1 0 1796895080 208064512 47103 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 50797 47103 145 145 0 50652 0 [pid=13910] vsize: 203188 Current children cumulated CPU time (s) 677.7 Current children cumulated vsize (Kb) 205312 [startup+690.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49383 0 0 0 68545 223 0 0 25 0 1 0 1796895080 208592896 47233 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 50926 47233 145 145 0 50781 0 [pid=13910] vsize: 203704 Current children cumulated CPU time (s) 687.69 Current children cumulated vsize (Kb) 205828 [startup+700.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49526 0 0 0 69543 225 0 0 25 0 1 0 1796895080 209166336 47376 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 51066 47376 145 145 0 50921 0 [pid=13910] vsize: 204264 Current children cumulated CPU time (s) 697.69 Current children cumulated vsize (Kb) 206388 [startup+710.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49636 0 0 0 70541 225 0 0 25 0 1 0 1796895080 209612800 47486 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 51175 47486 145 145 0 51030 0 [pid=13910] vsize: 204700 Current children cumulated CPU time (s) 707.67 Current children cumulated vsize (Kb) 206824 [startup+720.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49741 0 0 0 71540 226 0 0 25 0 1 0 1796895080 210030592 47591 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 51277 47591 145 145 0 51132 0 [pid=13910] vsize: 205108 Current children cumulated CPU time (s) 717.67 Current children cumulated vsize (Kb) 207232 [startup+730.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49910 0 0 0 72537 228 0 0 25 0 1 0 1796895080 210706432 47760 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 51442 47760 145 145 0 51297 0 [pid=13910] vsize: 205768 Current children cumulated CPU time (s) 727.66 Current children cumulated vsize (Kb) 207892 [startup+740.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50021 0 0 0 73535 229 0 0 25 0 1 0 1796895080 211156992 47871 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 51552 47871 145 145 0 51407 0 [pid=13910] vsize: 206208 Current children cumulated CPU time (s) 737.65 Current children cumulated vsize (Kb) 208332 [startup+750.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50156 0 0 0 74533 230 0 0 25 0 1 0 1796895080 211697664 48006 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 51684 48006 145 145 0 51539 0 [pid=13910] vsize: 206736 Current children cumulated CPU time (s) 747.64 Current children cumulated vsize (Kb) 208860 [startup+760.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50281 0 0 0 75531 230 0 0 25 0 1 0 1796895080 212230144 48131 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 51814 48131 145 145 0 51669 0 [pid=13910] vsize: 207256 Current children cumulated CPU time (s) 757.62 Current children cumulated vsize (Kb) 209380 [startup+770.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50419 0 0 0 76529 231 0 0 25 0 1 0 1796895080 212791296 48269 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 51951 48269 145 145 0 51806 0 [pid=13910] vsize: 207804 Current children cumulated CPU time (s) 767.61 Current children cumulated vsize (Kb) 209928 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50612 0 0 0 77525 233 0 0 25 0 1 0 1796895080 213569536 48462 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 52141 48462 145 145 0 51996 0 [pid=13910] vsize: 208564 Current children cumulated CPU time (s) 777.59 Current children cumulated vsize (Kb) 210688 [startup+790.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50756 0 0 0 78523 234 0 0 25 0 1 0 1796895080 214155264 48606 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 52284 48606 145 145 0 52139 0 [pid=13910] vsize: 209136 Current children cumulated CPU time (s) 787.58 Current children cumulated vsize (Kb) 211260 [startup+800.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50878 0 0 0 79521 234 0 0 25 0 1 0 1796895080 214646784 48728 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 52404 48728 145 145 0 52259 0 [pid=13910] vsize: 209616 Current children cumulated CPU time (s) 797.56 Current children cumulated vsize (Kb) 211740 [startup+810.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51021 0 0 0 80518 235 0 0 25 0 1 0 1796895080 215224320 48871 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 52545 48871 145 145 0 52400 0 [pid=13910] vsize: 210180 Current children cumulated CPU time (s) 807.54 Current children cumulated vsize (Kb) 212304 [startup+820.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51162 0 0 0 81516 236 0 0 25 0 1 0 1796895080 215797760 49012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 52685 49012 145 145 0 52540 0 [pid=13910] vsize: 210740 Current children cumulated CPU time (s) 817.53 Current children cumulated vsize (Kb) 212864 [startup+830.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51260 0 0 0 82514 237 0 0 25 0 1 0 1796895080 216190976 49110 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 52781 49110 145 145 0 52636 0 [pid=13910] vsize: 211124 Current children cumulated CPU time (s) 827.52 Current children cumulated vsize (Kb) 213248 [startup+840.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51385 0 0 0 83513 238 0 0 25 0 1 0 1796895080 216698880 49235 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 52905 49235 145 145 0 52760 0 [pid=13910] vsize: 211620 Current children cumulated CPU time (s) 837.52 Current children cumulated vsize (Kb) 213744 [startup+850.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51505 0 0 0 84511 238 0 0 25 0 1 0 1796895080 217186304 49355 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 53024 49355 145 145 0 52879 0 [pid=13910] vsize: 212096 Current children cumulated CPU time (s) 847.5 Current children cumulated vsize (Kb) 214220 [startup+860.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51633 0 0 0 85509 239 0 0 25 0 1 0 1796895080 217718784 49483 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 53154 49483 145 145 0 53009 0 [pid=13910] vsize: 212616 Current children cumulated CPU time (s) 857.49 Current children cumulated vsize (Kb) 214740 [startup+870.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51738 0 0 0 86507 240 0 0 25 0 1 0 1796895080 218140672 49588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 53257 49588 145 145 0 53112 0 [pid=13910] vsize: 213028 Current children cumulated CPU time (s) 867.48 Current children cumulated vsize (Kb) 215152 [startup+880.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51841 0 0 0 87505 241 0 0 25 0 1 0 1796895080 218570752 49691 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 53362 49691 145 145 0 53217 0 [pid=13910] vsize: 213448 Current children cumulated CPU time (s) 877.47 Current children cumulated vsize (Kb) 215572 [startup+890.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51994 0 0 0 88502 243 0 0 25 0 1 0 1796895080 219193344 49844 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 53514 49844 145 145 0 53369 0 [pid=13910] vsize: 214056 Current children cumulated CPU time (s) 887.46 Current children cumulated vsize (Kb) 216180 [startup+900.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52125 0 0 0 89501 243 0 0 25 0 1 0 1796895080 219713536 49975 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 53641 49975 145 145 0 53496 0 [pid=13910] vsize: 214564 Current children cumulated CPU time (s) 897.45 Current children cumulated vsize (Kb) 216688 [startup+910.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52235 0 0 0 90499 244 0 0 25 0 1 0 1796895080 220147712 50085 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 53747 50085 145 145 0 53602 0 [pid=13910] vsize: 214988 Current children cumulated CPU time (s) 907.44 Current children cumulated vsize (Kb) 217112 [startup+920.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52343 0 0 0 91497 245 0 0 25 0 1 0 1796895080 220585984 50193 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 53854 50193 145 145 0 53709 0 [pid=13910] vsize: 215416 Current children cumulated CPU time (s) 917.43 Current children cumulated vsize (Kb) 217540 [startup+930.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52447 0 0 0 92496 246 0 0 25 0 1 0 1796895080 220999680 50297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 53955 50297 145 145 0 53810 0 [pid=13910] vsize: 215820 Current children cumulated CPU time (s) 927.43 Current children cumulated vsize (Kb) 217944 [startup+940.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52509 0 0 0 93494 246 0 0 25 0 1 0 1796895080 221253632 50359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54017 50359 145 145 0 53872 0 [pid=13910] vsize: 216068 Current children cumulated CPU time (s) 937.41 Current children cumulated vsize (Kb) 218192 [startup+950.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52575 0 0 0 94493 247 0 0 25 0 1 0 1796895080 221519872 50425 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54082 50425 145 145 0 53937 0 [pid=13910] vsize: 216328 Current children cumulated CPU time (s) 947.41 Current children cumulated vsize (Kb) 218452 [startup+960.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52649 0 0 0 95491 248 0 0 17 0 1 0 1796895080 221822976 50499 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54156 50499 145 145 0 54011 0 [pid=13910] vsize: 216624 Current children cumulated CPU time (s) 957.4 Current children cumulated vsize (Kb) 218748 [startup+970.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52743 0 0 0 96489 249 0 0 25 0 1 0 1796895080 222203904 50593 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13910/statm): 54249 50593 145 145 0 54104 0 [pid=13910] vsize: 216996 Current children cumulated CPU time (s) 967.39 Current children cumulated vsize (Kb) 219120 [startup+980.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52887 0 0 0 97485 250 0 0 25 0 1 0 1796895080 222777344 50737 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54389 50737 145 145 0 54244 0 [pid=13910] vsize: 217556 Current children cumulated CPU time (s) 977.36 Current children cumulated vsize (Kb) 219680 [startup+990.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52979 0 0 0 98484 251 0 0 25 0 1 0 1796895080 223170560 50829 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54485 50829 145 145 0 54340 0 [pid=13910] vsize: 217940 Current children cumulated CPU time (s) 987.36 Current children cumulated vsize (Kb) 220064 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) T 13906 13906 22582 0 -1 0 53114 0 0 0 99481 252 0 0 25 0 1 0 1796895080 223707136 50964 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54616 50964 145 145 0 54471 0 [pid=13910] vsize: 218464 Current children cumulated CPU time (s) 997.34 Current children cumulated vsize (Kb) 220588 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53244 0 0 0 100479 253 0 0 25 0 1 0 1796895080 224231424 51094 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54744 51094 145 145 0 54599 0 [pid=13910] vsize: 218976 Current children cumulated CPU time (s) 1007.33 Current children cumulated vsize (Kb) 221100 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53339 0 0 0 101477 254 0 0 25 0 1 0 1796895080 224624640 51189 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54840 51189 145 145 0 54695 0 [pid=13910] vsize: 219360 Current children cumulated CPU time (s) 1017.32 Current children cumulated vsize (Kb) 221484 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53412 0 0 0 102476 254 0 0 25 0 1 0 1796895080 224927744 51262 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54914 51262 145 145 0 54769 0 [pid=13910] vsize: 219656 Current children cumulated CPU time (s) 1027.31 Current children cumulated vsize (Kb) 221780 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53492 0 0 0 103475 255 0 0 25 0 1 0 1796895080 225271808 51342 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 54998 51342 145 145 0 54853 0 [pid=13910] vsize: 219992 Current children cumulated CPU time (s) 1037.31 Current children cumulated vsize (Kb) 222116 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53552 0 0 0 104475 255 0 0 25 0 1 0 1796895080 225529856 51402 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55061 51402 145 145 0 54916 0 [pid=13910] vsize: 220244 Current children cumulated CPU time (s) 1047.31 Current children cumulated vsize (Kb) 222368 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53639 0 0 0 105473 256 0 0 25 0 1 0 1796895080 225894400 51489 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55150 51489 145 145 0 55005 0 [pid=13910] vsize: 220600 Current children cumulated CPU time (s) 1057.3 Current children cumulated vsize (Kb) 222724 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53737 0 0 0 106471 257 0 0 25 0 1 0 1796895080 226283520 51587 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55245 51587 145 145 0 55100 0 [pid=13910] vsize: 220980 Current children cumulated CPU time (s) 1067.29 Current children cumulated vsize (Kb) 223104 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53830 0 0 0 107471 258 0 0 25 0 1 0 1796895080 226684928 51680 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55343 51680 145 145 0 55198 0 [pid=13910] vsize: 221372 Current children cumulated CPU time (s) 1077.3 Current children cumulated vsize (Kb) 223496 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53937 0 0 0 108469 259 0 0 25 0 1 0 1796895080 227110912 51787 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55447 51787 145 145 0 55302 0 [pid=13910] vsize: 221788 Current children cumulated CPU time (s) 1087.29 Current children cumulated vsize (Kb) 223912 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54021 0 0 0 109468 260 0 0 25 0 1 0 1796895080 227442688 51871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55528 51871 145 145 0 55383 0 [pid=13910] vsize: 222112 Current children cumulated CPU time (s) 1097.29 Current children cumulated vsize (Kb) 224236 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54123 0 0 0 110466 260 0 0 25 0 1 0 1796895080 227848192 51973 4294967295 134512640 135094434 3221224432 3221223024 134557366 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55627 51973 145 145 0 55482 0 [pid=13910] vsize: 222508 Current children cumulated CPU time (s) 1107.27 Current children cumulated vsize (Kb) 224632 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54213 0 0 0 111464 262 0 0 25 0 1 0 1796895080 228216832 52063 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55717 52063 145 145 0 55572 0 [pid=13910] vsize: 222868 Current children cumulated CPU time (s) 1117.27 Current children cumulated vsize (Kb) 224992 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54278 0 0 0 112463 262 0 0 25 0 1 0 1796895080 228470784 52128 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55779 52128 145 145 0 55634 0 [pid=13910] vsize: 223116 Current children cumulated CPU time (s) 1127.26 Current children cumulated vsize (Kb) 225240 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54372 0 0 0 113462 263 0 0 25 0 1 0 1796895080 228851712 52222 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55872 52222 145 145 0 55727 0 [pid=13910] vsize: 223488 Current children cumulated CPU time (s) 1137.26 Current children cumulated vsize (Kb) 225612 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54460 0 0 0 114460 263 0 0 25 0 1 0 1796895080 229199872 52310 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 55957 52310 145 145 0 55812 0 [pid=13910] vsize: 223828 Current children cumulated CPU time (s) 1147.24 Current children cumulated vsize (Kb) 225952 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54531 0 0 0 115458 264 0 0 25 0 1 0 1796895080 229486592 52381 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 56027 52381 145 145 0 55882 0 [pid=13910] vsize: 224108 Current children cumulated CPU time (s) 1157.23 Current children cumulated vsize (Kb) 226232 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54595 0 0 0 116458 264 0 0 25 0 1 0 1796895080 229744640 52445 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 56090 52445 145 145 0 55945 0 [pid=13910] vsize: 224360 Current children cumulated CPU time (s) 1167.23 Current children cumulated vsize (Kb) 226484 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54673 0 0 0 117456 265 0 0 25 0 1 0 1796895080 230100992 52523 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 56177 52523 145 145 0 56032 0 [pid=13910] vsize: 224708 Current children cumulated CPU time (s) 1177.22 Current children cumulated vsize (Kb) 226832 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54729 0 0 0 118455 265 0 0 25 0 1 0 1796895080 230326272 52579 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 56232 52579 145 145 0 56087 0 [pid=13910] vsize: 224928 Current children cumulated CPU time (s) 1187.21 Current children cumulated vsize (Kb) 227052 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54793 0 0 0 119455 266 0 0 25 0 1 0 1796895080 230580224 52643 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 56294 52643 145 145 0 56149 0 [pid=13910] vsize: 225176 Current children cumulated CPU time (s) 1197.22 Current children cumulated vsize (Kb) 227300 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54866 0 0 0 120453 267 0 0 25 0 1 0 1796895080 230879232 52716 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 56367 52716 145 145 0 56222 0 [pid=13910] vsize: 225468 Current children cumulated CPU time (s) 1207.21 Current children cumulated vsize (Kb) 227592 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13910 Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13906/statm): 531 226 485 147 0 384 0 [pid=13906] vsize: 2124 Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54866 0 0 0 120453 267 0 0 25 0 1 0 1796895080 230879232 52716 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13910/statm): 56367 52716 145 145 0 56222 0 [pid=13910] vsize: 225468 Current children cumulated CPU time (s) 1207.21 Current children cumulated vsize (Kb) 227592 Sending SIGTERM to -13906 Sleeping 2 seconds One traced child (pid=13906) ended because it received signal 15 (SIGTERM) One traced child (pid=13910) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.19 CPU time (s): 1207.31 CPU user time (s): 1204.53 CPU system time (s): 2.77658 CPU usage (%): 99.762 Max. virtual memory (cumulated for all children) (Kb): 227592
ERROR: no interpretation found !