Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-standgub.opb |
MD5SUM | 4278f4b256e2a8fa799a6ca1554251b3 |
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 | 140 |
Biggest coefficient in the objective function | 52428800 |
Number of bits for the biggest coefficient in the objective function | 26 |
Sum of the numbers in the objective function | 318766800 |
Number of bits of the sum of numbers in the objective function | 29 |
Biggest number in a constraint | 75573493760 |
Number of bits of the biggest number in a constraint | 37 |
Biggest sum of numbers in a constraint | 2374370081400 |
Number of bits of the biggest sum of numbers | 42 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 22302 |
Total number of constraints | 463 |
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 | 463 |
Minimum length of a constraint | 8 |
Maximum length of a constraint | 14900 |
LAUNCH ON wulflinc1 THE 2005-09-20 03:02:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3222 boxname=wulflinc1 idbench=878 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4278f4b256e2a8fa799a6ca1554251b3 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-standgub.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-standgub.opb IDLAUNCH: 3222 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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: 901444 kB Buffers: 3572 kB Cached: 100120 kB SwapCached: 1164 kB Active: 32944 kB Inactive: 73276 kB HighTotal: 131008 kB HighFree: 27076 kB LowTotal: 903652 kB LowFree: 874368 kB SwapTotal: 2097136 kB SwapFree: 2095232 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 21080 kB Committed_AS: 92628 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:23:07 (client local time) WITH STATUS 0 IN 1208.79 SECONDS stats: 3222 7 1208.79 0
c Parsing PB file... c Converting 596 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ################################################################################################################################################################ c -- Clauses(.)/Splits(s): sssssssssssssss c ---[ 607]---> BDD-cost: 13 c ---[ 606]---> BDD-cost: 12 c ---[ 605]---> BDD-cost: 12 c ---[ 604]---> BDD-cost: 10 c ---[ 603]---> BDD-cost: 10 c ---[ 602]---> BDD-cost: 14 c ---[ 601]---> BDD-cost: 13 c ---[ 600]---> BDD-cost: 12 c ---[ 599]---> BDD-cost: 12 c ---[ 598]---> BDD-cost: 10 c ---[ 597]---> BDD-cost: 10 c ---[ 596]---> BDD-cost: 14 c ---[ 595]---> BDD-cost: 13 c ---[ 594]---> BDD-cost: 12 c ---[ 593]---> BDD-cost: 12 c ---[ 592]---> BDD-cost: 10 c ---[ 591]---> BDD-cost: 10 c ---[ 590]---> BDD-cost: 14 c ---[ 589]---> BDD-cost: 13 c ---[ 588]---> BDD-cost: 12 c ---[ 587]---> BDD-cost: 12 c ---[ 586]---> BDD-cost: 10 c ---[ 585]---> BDD-cost: 10 c ---[ 584]---> BDD-cost: 14 c ---[ 583]---> BDD-cost: 13 c ---[ 582]---> BDD-cost: 12 c ---[ 581]---> BDD-cost: 12 c ---[ 580]---> BDD-cost: 10 c ---[ 579]---> BDD-cost: 10 c ---[ 578]---> BDD-cost: 14 c ---[ 577]---> BDD-cost: 13 c ---[ 576]---> BDD-cost: 12 c ---[ 575]---> BDD-cost: 12 c ---[ 574]---> BDD-cost: 10 c ---[ 573]---> BDD-cost: 10 c ---[ 572]---> BDD-cost: 14 c ---[ 571]---> BDD-cost: 10 c ---[ 570]---> BDD-cost: 10 c ---[ 569]---> BDD-cost: 10 c ---[ 565]---> BDD-cost: 10 c ---[ 564]---> BDD-cost: 10 c ---[ 563]---> BDD-cost: 10 c ---[ 559]---> BDD-cost: 7 c ---[ 557]---> BDD-cost: 7 c ---[ 556]---> BDD-cost: 7 c ---[ 554]---> BDD-cost: 7 c ---[ 553]---> BDD-cost: 7 c ---[ 552]---> BDD-cost: 7 c ---[ 550]---> BDD-cost: 7 c ---[ 549]---> BDD-cost: 7 c ---[ 548]---> BDD-cost: 7 c ---[ 547]---> BDD-cost: 7 c ---[ 545]---> BDD-cost: 7 c ---[ 544]---> BDD-cost: 7 c ---[ 543]---> BDD-cost: 7 c ---[ 542]---> BDD-cost: 7 c ---[ 541]---> BDD-cost: 7 c ---[ 540]---> BDD-cost: 7 c ---[ 539]---> BDD-cost: 7 c ---[ 538]---> BDD-cost: 7 c ---[ 537]---> BDD-cost: 7 c ---[ 536]---> BDD-cost: 7 c ---[ 535]---> BDD-cost: 7 c ---[ 534]---> BDD-cost: 7 c ---[ 533]---> BDD-cost: 7 c ---[ 532]---> BDD-cost: 7 c ---[ 530]---> BDD-cost: 7 c ---[ 529]---> BDD-cost: 7 c ---[ 528]---> BDD-cost: 7 c ---[ 526]---> BDD-cost: 7 c ---[ 525]---> BDD-cost: 7 c ---[ 524]---> BDD-cost: 7 c ---[ 522]---> BDD-cost: 7 c ---[ 521]---> BDD-cost: 7 c ---[ 520]---> BDD-cost: 7 c ---[ 519]---> BDD-cost: 7 c ---[ 517]---> BDD-cost: 7 c ---[ 516]---> BDD-cost: 7 c ---[ 515]---> BDD-cost: 7 c ---[ 514]---> BDD-cost: 7 c ---[ 513]---> BDD-cost: 7 c ---[ 512]---> BDD-cost: 7 c ---[ 511]---> BDD-cost: 7 c ---[ 510]---> BDD-cost: 7 c ---[ 509]---> BDD-cost: 7 c ---[ 508]---> BDD-cost: 7 c ---[ 507]---> BDD-cost: 7 c ---[ 506]---> BDD-cost: 7 c ---[ 505]---> BDD-cost: 7 c ---[ 504]---> BDD-cost: 7 c ---[ 502]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 500]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 498]---> Sorter-cost: 807 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 496]---> Sorter-cost: 807 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 494]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 492]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 490]---> Sorter-cost: 807 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 488]---> Sorter-cost: 807 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 486]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 482]---> Sorter-cost: 807 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 480]---> Sorter-cost: 807 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 478]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 476]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 474]---> Adder-cost: 276 maxlim: 65534 bits: 17/16 c ---[ 472]---> Adder-cost: 295 maxlim: 65534 bits: 17/16 c ---[ 470]---> Adder-cost: 276 maxlim: 65534 bits: 17/16 c ---[ 468]---> Adder-cost: 295 maxlim: 65534 bits: 17/16 c ---[ 466]---> Adder-cost: 408 maxlim: 65535 bits: 17/16 c ---[ 464]---> Adder-cost: 405 maxlim: 65535 bits: 17/16 c ---[ 462]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 460]---> Adder-cost: 318 maxlim: 135165 bits: 18/18 c ---[ 458]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 456]---> Adder-cost: 318 maxlim: 135165 bits: 18/18 c ---[ 454]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 452]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 450]---> Adder-cost: 294 maxlim: 67581 bits: 17/17 c ---[ 448]---> Adder-cost: 338 maxlim: 69629 bits: 18/17 c ---[ 446]---> Adder-cost: 294 maxlim: 67581 bits: 17/17 c ---[ 444]---> Adder-cost: 338 maxlim: 69629 bits: 18/17 c ---[ 442]---> Adder-cost: 408 maxlim: 65535 bits: 17/16 c ---[ 440]---> Adder-cost: 405 maxlim: 65535 bits: 17/16 c ---[ 438]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 436]---> Adder-cost: 344 maxlim: 147453 bits: 19/18 c ---[ 434]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 432]---> Adder-cost: 344 maxlim: 147453 bits: 19/18 c ---[ 430]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 428]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 426]---> Adder-cost: 294 maxlim: 67581 bits: 17/17 c ---[ 424]---> Adder-cost: 360 maxlim: 81917 bits: 18/17 c ---[ 422]---> Adder-cost: 294 maxlim: 67581 bits: 17/17 c ---[ 420]---> Adder-cost: 360 maxlim: 81917 bits: 18/17 c ---[ 418]---> Adder-cost: 408 maxlim: 65535 bits: 17/16 c ---[ 416]---> Adder-cost: 405 maxlim: 65535 bits: 17/16 c ---[ 414]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 412]---> Adder-cost: 362 maxlim: 163837 bits: 19/18 c ---[ 410]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 408]---> Adder-cost: 362 maxlim: 163837 bits: 19/18 c ---[ 406]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 404]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 402]---> Adder-cost: 276 maxlim: 65534 bits: 17/16 c ---[ 400]---> Adder-cost: 295 maxlim: 65534 bits: 17/16 c ---[ 398]---> Adder-cost: 276 maxlim: 65534 bits: 17/16 c ---[ 396]---> Adder-cost: 295 maxlim: 65534 bits: 17/16 c ---[ 394]---> Adder-cost: 408 maxlim: 65535 bits: 17/16 c ---[ 392]---> Adder-cost: 405 maxlim: 65535 bits: 17/16 c ---[ 390]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 388]---> Adder-cost: 318 maxlim: 135165 bits: 18/18 c ---[ 386]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 384]---> Adder-cost: 318 maxlim: 135165 bits: 18/18 c ---[ 382]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 380]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 378]---> Adder-cost: 294 maxlim: 67581 bits: 17/17 c ---[ 376]---> Adder-cost: 338 maxlim: 69629 bits: 18/17 c ---[ 374]---> Adder-cost: 294 maxlim: 67581 bits: 17/17 c ---[ 372]---> Adder-cost: 338 maxlim: 69629 bits: 18/17 c ---[ 370]---> Adder-cost: 408 maxlim: 65535 bits: 17/16 c ---[ 368]---> Adder-cost: 405 maxlim: 65535 bits: 17/16 c ---[ 366]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 364]---> Adder-cost: 344 maxlim: 147453 bits: 19/18 c ---[ 362]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 360]---> Adder-cost: 344 maxlim: 147453 bits: 19/18 c ---[ 358]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 356]---> Adder-cost: 382 maxlim: 32767 bits: 16/15 c ---[ 354]---> Adder-cost: 294 maxlim: 67581 bits: 17/17 c ---[ 352]---> Adder-cost: 360 maxlim: 81917 bits: 18/17 c ---[ 350]---> Adder-cost: 294 maxlim: 67581 bits: 17/17 c ---[ 348]---> Adder-cost: 360 maxlim: 81917 bits: 18/17 c ---[ 346]---> Adder-cost: 408 maxlim: 65535 bits: 17/16 c ---[ 344]---> Adder-cost: 405 maxlim: 65535 bits: 17/16 c ---[ 342]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 340]---> Adder-cost: 362 maxlim: 163837 bits: 19/18 c ---[ 338]---> Adder-cost: 298 maxlim: 133117 bits: 18/18 c ---[ 336]---> Adder-cost: 362 maxlim: 163837 bits: 19/18 c ---[ 334]---> BDD-cost: 31 c ---[ 332]---> BDD-cost: 34 c ---[ 330]---> BDD-cost: 31 c ---[ 328]---> BDD-cost: 34 c ---[ 326]---> BDD-cost: 31 c ---[ 324]---> BDD-cost: 34 c ---[ 322]---> BDD-cost: 31 c ---[ 320]---> BDD-cost: 34 c ---[ 318]---> BDD-cost: 91 c ---[ 316]---> Sorter-cost: 496 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 314]---> BDD-cost: 91 c ---[ 312]---> Sorter-cost: 496 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 310]---> BDD-cost: 31 c ---[ 308]---> BDD-cost: 40 c ---[ 306]---> BDD-cost: 31 c ---[ 304]---> BDD-cost: 40 c ---[ 302]---> BDD-cost: 91 c ---[ 300]---> Sorter-cost: 494 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 298]---> BDD-cost: 91 c ---[ 296]---> Sorter-cost: 494 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 294]---> BDD-cost: 31 c ---[ 292]---> BDD-cost: 43 c ---[ 290]---> BDD-cost: 31 c ---[ 288]---> BDD-cost: 43 c ---[ 286]---> Adder-cost: 3650 maxlim: 6944215190 bits: 34/33 c ---[ 284]---> Adder-cost: 1968 maxlim: 1425264 bits: 22/21 c ---[ 283]---> Adder-cost: 758 maxlim: 8556339 bits: 25/24 c ---[ 282]---> Adder-cost: 941 maxlim: 13112437 bits: 25/24 c ---[ 281]---> Adder-cost: 847 maxlim: 12840657 bits: 25/24 c ---[ 279]---> Adder-cost: 584 maxlim: 1241022 bits: 22/21 c ---[ 277]---> Adder-cost: 72306 maxlim: 8075354693 bits: 33/33 c ---[ 276]---> BDD-cost: 87 c ---[ 275]---> BDD-cost: 96 c ---[ 274]---> BDD-cost: 87 c ---[ 273]---> BDD-cost: 96 c ---[ 272]---> BDD-cost: 87 c ---[ 271]---> BDD-cost: 96 c ---[ 270]---> BDD-cost: 87 c ---[ 269]---> BDD-cost: 96 c ---[ 268]---> BDD-cost: 87 c ---[ 267]---> BDD-cost: 114 c ---[ 266]---> BDD-cost: 87 c ---[ 265]---> BDD-cost: 114 c ---[ 264]---> BDD-cost: 87 c ---[ 263]---> BDD-cost: 114 c ---[ 262]---> BDD-cost: 87 c ---[ 261]---> BDD-cost: 114 c ---[ 260]---> BDD-cost: 87 c ---[ 259]---> BDD-cost: 123 c ---[ 258]---> BDD-cost: 87 c ---[ 257]---> BDD-cost: 123 c ---[ 256]---> BDD-cost: 87 c ---[ 255]---> BDD-cost: 123 c ---[ 254]---> BDD-cost: 87 c ---[ 253]---> BDD-cost: 123 c ---[ 251]---> Sorter-cost: 483 Base: 2 2 2 3 5 2 2 2 c ---[ 249]---> Sorter-cost: 483 Base: 2 2 2 3 5 2 2 2 c ---[ 247]---> Sorter-cost: 483 Base: 2 2 2 3 5 2 2 2 c ---[ 245]---> Sorter-cost: 483 Base: 2 2 2 3 5 2 2 2 c ---[ 243]---> Sorter-cost: 483 Base: 2 2 2 3 5 2 2 2 c ---[ 241]---> Sorter-cost: 483 Base: 2 2 2 3 5 2 2 2 c ---[ 240]---> BDD-cost: 3 c ---[ 239]---> BDD-cost: 71 c ---[ 238]---> BDD-cost: 3 c ---[ 237]---> BDD-cost: 71 c ---[ 235]---> BDD-cost: 71 c ---[ 233]---> BDD-cost: 71 c ---[ 231]---> BDD-cost: 71 c ---[ 229]---> BDD-cost: 71 c ---[ 228]---> BDD-cost: 0 c ---[ 227]---> BDD-cost: 22 c ---[ 226]---> BDD-cost: 22 c ---[ 225]---> BDD-cost: 63 c ---[ 224]---> BDD-cost: 63 c ---[ 223]---> Sorter-cost: 178 Base: 2 2 2 2 2 2 2 2 2 c ---[ 222]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 221]---> BDD-cost: 10 c ---[ 220]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 219]---> BDD-cost: 10 c ---[ 218]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 217]---> BDD-cost: 10 c ---[ 216]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> BDD-cost: 23 c ---[ 207]---> BDD-cost: 73 c ---[ 206]---> BDD-cost: 73 c ---[ 204]---> Sorter-cost: 548 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 202]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 200]---> BDD-cost: 132 c ---[ 198]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 196]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 194]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 192]---> BDD-cost: 132 c ---[ 190]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 188]---> Sorter-cost: 579 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 186]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 184]---> BDD-cost: 136 c ---[ 182]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 180]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 178]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 588 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 174]---> Sorter-cost: 588 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 172]---> Sorter-cost: 548 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 579 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 154]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 152]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 150]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 148]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 146]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 144]---> Sorter-cost: 588 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 142]---> Sorter-cost: 588 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 140]---> Sorter-cost: 548 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 138]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 136]---> BDD-cost: 132 c ---[ 134]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 132]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 130]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 128]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 124]---> Sorter-cost: 579 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 122]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> BDD-cost: 136 c ---[ 118]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 116]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> Sorter-cost: 588 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 588 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 109]---> BDD-cost: 11 c ---[ 108]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> BDD-cost: 11 c ---[ 102]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 100]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 98]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 97]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 96]---> BDD-cost: 11 c ---[ 95]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 94]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 93]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 91]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 90]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 89]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 88]---> BDD-cost: 11 c ---[ 87]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 86]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 85]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 84]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 83]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 82]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 81]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 80]---> BDD-cost: 11 c ---[ 79]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 78]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 77]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 76]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 75]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 74]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 73]---> BDD-cost: 11 c ---[ 72]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 71]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 70]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 68]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 67]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 66]---> BDD-cost: 3 c ---[ 65]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 62]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> BDD-cost: 3 c ---[ 59]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> BDD-cost: 3 c ---[ 52]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 50]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 48]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 46]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> BDD-cost: 3 c ---[ 44]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 37]---> BDD-cost: 3 c ---[ 36]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> BDD-cost: 3 c ---[ 29]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 27]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> Adder-cost: 700 maxlim: 144219 bits: 18/18 c ---[ 22]---> Adder-cost: 816 maxlim: 294875 bits: 19/19 c ---[ 21]---> Adder-cost: 700 maxlim: 144219 bits: 18/18 c ---[ 20]---> Adder-cost: 816 maxlim: 294875 bits: 19/19 c ---[ 19]---> Adder-cost: 840 maxlim: 144219 bits: 18/18 c ---[ 18]---> Adder-cost: 1058 maxlim: 589787 bits: 20/20 c ---[ 17]---> Adder-cost: 840 maxlim: 144219 bits: 18/18 c ---[ 16]---> Adder-cost: 1058 maxlim: 589787 bits: 20/20 c ---[ 15]---> Adder-cost: 840 maxlim: 144219 bits: 18/18 c ---[ 14]---> Adder-cost: 1164 maxlim: 1179611 bits: 21/21 c ---[ 13]---> Adder-cost: 840 maxlim: 144219 bits: 18/18 c ---[ 12]---> Adder-cost: 1164 maxlim: 1179611 bits: 21/21 c ---[ 11]---> BDD-cost: 7 c ---[ 10]---> BDD-cost: 7 c ---[ 9]---> BDD-cost: 7 c ---[ 8]---> BDD-cost: 7 c ---[ 7]---> BDD-cost: 7 c ---[ 6]---> BDD-cost: 7 c ---[ 5]---> BDD-cost: 7 c ---[ 4]---> BDD-cost: 7 c ---[ 3]---> BDD-cost: 22 c ---[ 2]---> BDD-cost: 22 c ---[ 1]---> BDD-cost: 22 c ---[ 0]---> BDD-cost: 22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 964494 3250947 | 321498 0 0 nan | 0.000 % | c | 100 | 964478 3250895 | 353647 98 304 3.1 | 6.740 % | c | 250 | 964106 3249786 | 389012 228 797 3.5 | 6.781 % | c | 475 | 964002 3249529 | 427913 433 1737 4.0 | 6.796 % | c | 812 | 963795 3248800 | 470705 742 2871 3.9 | 6.814 % | c | 1318 | 963702 3248475 | 517775 1231 4855 3.9 | 6.821 % | c | 2077 | 963366 3247410 | 569553 1936 7861 4.1 | 6.854 % | c | 3216 | 963175 3246814 | 626508 3033 17391 5.7 | 6.874 % | c | 4925 | 962759 3245603 | 689159 4650 34938 7.5 | 6.918 % | c | 7487 | 962250 3243978 | 758075 7143 61280 8.6 | 6.959 % | c | 11332 | 958155 3233897 | 833883 10842 111683 10.3 | 7.464 % | c | 17098 | 951800 3218279 | 917271 16238 163430 10.1 | 8.278 % | c | 25747 | 942821 3195619 | 1008998 23980 230144 9.6 | 9.447 % | c | 38722 | 941216 3191324 | 1109898 36800 1169188 31.8 | 9.616 % | c | 58186 | 940987 3190590 | 1220888 56246 2436269 43.3 | 9.632 % |
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/20349/stat): 20349 (minisat+_script) R 20348 20349 10120 0 -1 0 18 0 0 0 0 0 0 0 21 0 1 0 1740061742 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/20349/statm): 174 3 169 147 0 27 0 [pid=20349] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/i686/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libdl.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libdl.so.2 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/lib/locale/locale-archive open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script open syscall for file /usr/lib/gconv/gconv-modules.cache New process pid=20350 New process pid=20351 New process pid=20352 execve syscall for /bin/sed executable One traced child (pid=20351) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/i686/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/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 open syscall for file /usr/lib/locale/locale-archive open syscall for file /usr/lib/gconv/gconv-modules.cache One traced child (pid=20352) exited with status: 0 One traced child (pid=20350) exited with status: 0 New process pid=20353 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-standgub.opb [startup+10.0033 s] Raw data (loadavg): 0.76 0.92 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 4324 0 0 0 961 16 0 0 25 0 1 0 1740061749 15196160 3209 4294967295 134512640 135094434 3221221600 3221169040 134597176 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20353/statm): 3710 3209 145 145 0 3565 0 [pid=20353] vsize: 14840 Current children cumulated CPU time (s) 9.77 Current children cumulated vsize (Kb) 19036 [startup+20.0041 s] Raw data (loadavg): 0.79 0.93 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 1914 43 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216744 134677377 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 19.57 Current children cumulated vsize (Kb) 30488 [startup+30.0049 s] Raw data (loadavg): 0.82 0.93 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 2914 43 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217040 134599970 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 29.57 Current children cumulated vsize (Kb) 30488 [startup+40.0047 s] Raw data (loadavg): 0.85 0.93 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 3915 43 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216928 134677086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 39.58 Current children cumulated vsize (Kb) 30488 [startup+50.0055 s] Raw data (loadavg): 0.87 0.93 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 4914 44 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216864 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 49.58 Current children cumulated vsize (Kb) 30488 [startup+60.0062 s] Raw data (loadavg): 0.89 0.93 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 5914 44 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217216 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 59.58 Current children cumulated vsize (Kb) 30488 [startup+70.007 s] Raw data (loadavg): 0.91 0.94 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 6914 44 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134677278 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 69.58 Current children cumulated vsize (Kb) 30488 [startup+80.0078 s] Raw data (loadavg): 0.92 0.94 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 7914 44 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217664 134677099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 79.58 Current children cumulated vsize (Kb) 30488 [startup+90.0086 s] Raw data (loadavg): 0.93 0.94 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 8914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217312 134677065 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 89.59 Current children cumulated vsize (Kb) 30488 [startup+100.009 s] Raw data (loadavg): 0.94 0.94 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 9914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134601029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 99.59 Current children cumulated vsize (Kb) 30488 [startup+110.01 s] Raw data (loadavg): 0.95 0.94 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 10914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217920 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 109.59 Current children cumulated vsize (Kb) 30488 [startup+120.01 s] Raw data (loadavg): 0.96 0.94 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 11914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217468 134677081 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 119.59 Current children cumulated vsize (Kb) 30488 [startup+130.011 s] Raw data (loadavg): 0.96 0.94 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 12914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217568 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 129.59 Current children cumulated vsize (Kb) 30488 [startup+140.012 s] Raw data (loadavg): 0.97 0.95 0.92 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 13915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217216 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 139.6 Current children cumulated vsize (Kb) 30488 [startup+150.013 s] Raw data (loadavg): 1.05 0.96 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 14915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217312 134677021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 149.6 Current children cumulated vsize (Kb) 30488 [startup+160.014 s] Raw data (loadavg): 1.04 0.96 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 15915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 159.6 Current children cumulated vsize (Kb) 30488 [startup+170.014 s] Raw data (loadavg): 1.04 0.96 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 16915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218096 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 169.6 Current children cumulated vsize (Kb) 30488 [startup+180.015 s] Raw data (loadavg): 1.03 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 17915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217360 134519504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 179.6 Current children cumulated vsize (Kb) 30488 [startup+190.014 s] Raw data (loadavg): 1.03 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 18915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 189.6 Current children cumulated vsize (Kb) 30488 [startup+200.015 s] Raw data (loadavg): 1.02 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 19916 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217452 134676460 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 199.61 Current children cumulated vsize (Kb) 30488 [startup+210.016 s] Raw data (loadavg): 1.02 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 20916 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 209.61 Current children cumulated vsize (Kb) 30488 [startup+220.016 s] Raw data (loadavg): 1.01 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 21916 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218096 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 219.61 Current children cumulated vsize (Kb) 30488 [startup+230.017 s] Raw data (loadavg): 1.01 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 22916 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218448 134677310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 229.62 Current children cumulated vsize (Kb) 30488 [startup+240.016 s] Raw data (loadavg): 1.01 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 23916 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217112 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 239.62 Current children cumulated vsize (Kb) 30488 [startup+250.017 s] Raw data (loadavg): 1.01 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 24916 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217216 134677239 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 249.62 Current children cumulated vsize (Kb) 30488 [startup+260.018 s] Raw data (loadavg): 1.01 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 25917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217664 134677035 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 259.63 Current children cumulated vsize (Kb) 30488 [startup+270.018 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 26917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217744 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 269.63 Current children cumulated vsize (Kb) 30488 [startup+280.019 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 27917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218368 134676294 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 279.63 Current children cumulated vsize (Kb) 30488 [startup+290.018 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 28917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217744 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 289.63 Current children cumulated vsize (Kb) 30488 [startup+300.019 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 29917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217920 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 299.63 Current children cumulated vsize (Kb) 30488 [startup+310.02 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 30917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217728 134600246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 309.63 Current children cumulated vsize (Kb) 30488 [startup+320.02 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 31918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217744 134600151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 319.64 Current children cumulated vsize (Kb) 30488 [startup+330.021 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 32917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218272 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 329.63 Current children cumulated vsize (Kb) 30488 [startup+340.02 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 33918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218096 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 339.64 Current children cumulated vsize (Kb) 30488 [startup+350.021 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 34918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218168 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 349.64 Current children cumulated vsize (Kb) 30488 [startup+360.022 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 35918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217920 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 359.64 Current children cumulated vsize (Kb) 30488 [startup+370.022 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 36918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218272 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 369.64 Current children cumulated vsize (Kb) 30488 [startup+380.022 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 37919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218172 134677081 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 379.65 Current children cumulated vsize (Kb) 30488 [startup+390.023 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 38919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216336 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 389.65 Current children cumulated vsize (Kb) 30488 [startup+400.024 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 39919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216688 134677333 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 399.65 Current children cumulated vsize (Kb) 30488 [startup+410.025 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 40919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217136 134677099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 409.65 Current children cumulated vsize (Kb) 30488 [startup+420.026 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 41919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217920 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 419.65 Current children cumulated vsize (Kb) 30488 [startup+430.026 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 42920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218368 134676251 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 429.66 Current children cumulated vsize (Kb) 30488 [startup+440.026 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 43920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217568 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 439.66 Current children cumulated vsize (Kb) 30488 [startup+450.028 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 44920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218096 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 449.66 Current children cumulated vsize (Kb) 30488 [startup+460.029 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 45920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218156 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 459.66 Current children cumulated vsize (Kb) 30488 [startup+470.029 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 46920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218544 134677069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 469.66 Current children cumulated vsize (Kb) 30488 [startup+480.029 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 47921 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218272 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 479.67 Current children cumulated vsize (Kb) 30488 [startup+490.03 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 48921 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218624 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 489.67 Current children cumulated vsize (Kb) 30488 [startup+500.031 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 49921 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134676480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 499.67 Current children cumulated vsize (Kb) 30488 [startup+510.032 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 50921 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217816 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 509.67 Current children cumulated vsize (Kb) 30488 [startup+520.033 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 51922 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 519.68 Current children cumulated vsize (Kb) 30488 [startup+530.033 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 52922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217312 134677007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 529.69 Current children cumulated vsize (Kb) 30488 [startup+540.033 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 53922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217804 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 539.69 Current children cumulated vsize (Kb) 30488 [startup+550.034 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 54922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217744 134677310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 549.69 Current children cumulated vsize (Kb) 30488 [startup+560.035 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 55922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218272 134600291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 559.69 Current children cumulated vsize (Kb) 30488 [startup+570.035 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 56922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218440 134600155 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 569.69 Current children cumulated vsize (Kb) 30488 [startup+580.036 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 57923 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218252 134676382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 579.7 Current children cumulated vsize (Kb) 30488 [startup+590.037 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 58923 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218976 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0 [pid=20353] vsize: 26292 Current children cumulated CPU time (s) 589.7 Current children cumulated vsize (Kb) 30488 [startup+600.038 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12310 0 0 0 59923 47 0 0 25 0 1 0 1740061749 27090944 6054 4294967295 134512640 135094434 3221221600 3221219024 134676465 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6614 6054 145 145 0 6469 0 [pid=20353] vsize: 26456 Current children cumulated CPU time (s) 599.7 Current children cumulated vsize (Kb) 30652 [startup+610.039 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12310 0 0 0 60923 47 0 0 25 0 1 0 1740061749 27090944 6054 4294967295 134512640 135094434 3221221600 3221218444 134600233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 6614 6054 145 145 0 6469 0 [pid=20353] vsize: 26456 Current children cumulated CPU time (s) 609.7 Current children cumulated vsize (Kb) 30652 [startup+620.038 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 61919 51 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221217920 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 619.7 Current children cumulated vsize (Kb) 33852 [startup+630.039 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 62920 51 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221217972 134677232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 629.71 Current children cumulated vsize (Kb) 33852 [startup+640.039 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 63920 51 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218096 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 639.71 Current children cumulated vsize (Kb) 33852 [startup+650.04 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 64919 52 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218272 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 649.71 Current children cumulated vsize (Kb) 33852 [startup+660.04 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 65919 52 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218368 134677059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 659.71 Current children cumulated vsize (Kb) 33852 [startup+670.04 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 66919 52 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218272 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 669.71 Current children cumulated vsize (Kb) 33852 [startup+680.041 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 67919 52 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219072 134677059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 679.71 Current children cumulated vsize (Kb) 33852 [startup+690.042 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 68919 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218800 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 689.72 Current children cumulated vsize (Kb) 33852 [startup+700.043 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 69919 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219504 134600215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 699.72 Current children cumulated vsize (Kb) 33852 [startup+710.043 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 70919 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219152 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 709.72 Current children cumulated vsize (Kb) 33852 [startup+720.043 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 71920 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219220 134676335 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 719.73 Current children cumulated vsize (Kb) 33852 [startup+730.044 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 72920 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219600 134677042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0 [pid=20353] vsize: 29656 Current children cumulated CPU time (s) 729.73 Current children cumulated vsize (Kb) 33852 [startup+740.044 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 15790 0 0 0 73915 57 0 0 25 0 1 0 1740061749 38912000 8875 4294967295 134512640 135094434 3221221600 3221219088 134519056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 9500 8875 145 145 0 9355 0 [pid=20353] vsize: 38000 Current children cumulated CPU time (s) 739.72 Current children cumulated vsize (Kb) 42196 [startup+750.045 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35509 0 0 0 74775 128 0 0 25 0 1 0 1740061749 117919744 27184 4294967295 134512640 135094434 3221221600 3221220260 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20353/statm): 28789 27184 145 145 0 28644 0 [pid=20353] vsize: 115156 Current children cumulated CPU time (s) 749.03 Current children cumulated vsize (Kb) 119352 [startup+760.045 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35511 0 0 0 75774 129 0 0 25 0 1 0 1740061749 117927936 27186 4294967295 134512640 135094434 3221221600 3221220288 134558987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20353/statm): 28791 27186 145 145 0 28646 0 [pid=20353] vsize: 115164 Current children cumulated CPU time (s) 759.03 Current children cumulated vsize (Kb) 119360 [startup+770.046 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35604 0 0 0 76772 130 0 0 25 0 1 0 1740061749 118308864 27279 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 28884 27279 145 145 0 28739 0 [pid=20353] vsize: 115536 Current children cumulated CPU time (s) 769.02 Current children cumulated vsize (Kb) 119732 [startup+780.047 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35660 0 0 0 77771 130 0 0 25 0 1 0 1740061749 118538240 27335 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 28940 27335 145 145 0 28795 0 [pid=20353] vsize: 115760 Current children cumulated CPU time (s) 779.01 Current children cumulated vsize (Kb) 119956 [startup+790.048 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35722 0 0 0 78770 131 0 0 25 0 1 0 1740061749 118792192 27397 4294967295 134512640 135094434 3221221600 3221220276 134553436 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29002 27397 145 145 0 28857 0 [pid=20353] vsize: 116008 Current children cumulated CPU time (s) 789.01 Current children cumulated vsize (Kb) 120204 [startup+800.049 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35825 0 0 0 79769 131 0 0 25 0 1 0 1740061749 119218176 27500 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29106 27500 145 145 0 28961 0 [pid=20353] vsize: 116424 Current children cumulated CPU time (s) 799 Current children cumulated vsize (Kb) 120620 [startup+810.049 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35867 0 0 0 80768 131 0 0 25 0 1 0 1740061749 119386112 27542 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20353/statm): 29147 27542 145 145 0 29002 0 [pid=20353] vsize: 116588 Current children cumulated CPU time (s) 808.99 Current children cumulated vsize (Kb) 120784 [startup+820.049 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35929 0 0 0 81767 132 0 0 25 0 1 0 1740061749 119672832 27604 4294967295 134512640 135094434 3221221600 3221220260 134553475 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20353/statm): 29217 27604 145 145 0 29072 0 [pid=20353] vsize: 116868 Current children cumulated CPU time (s) 818.99 Current children cumulated vsize (Kb) 121064 [startup+830.05 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35975 0 0 0 82765 133 0 0 25 0 1 0 1740061749 119853056 27650 4294967295 134512640 135094434 3221221600 3221220260 134553450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29261 27650 145 145 0 29116 0 [pid=20353] vsize: 117044 Current children cumulated CPU time (s) 828.98 Current children cumulated vsize (Kb) 121240 [startup+840.051 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36029 0 0 0 83765 133 0 0 25 0 1 0 1740061749 120070144 27704 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29314 27704 145 145 0 29169 0 [pid=20353] vsize: 117256 Current children cumulated CPU time (s) 838.98 Current children cumulated vsize (Kb) 121452 [startup+850.052 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36057 0 0 0 84764 134 0 0 25 0 1 0 1740061749 120184832 27732 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29342 27732 145 145 0 29197 0 [pid=20353] vsize: 117368 Current children cumulated CPU time (s) 848.98 Current children cumulated vsize (Kb) 121564 [startup+860.052 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36111 0 0 0 85763 134 0 0 25 0 1 0 1740061749 120397824 27786 4294967295 134512640 135094434 3221221600 3221220304 134559019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29394 27786 145 145 0 29249 0 [pid=20353] vsize: 117576 Current children cumulated CPU time (s) 858.97 Current children cumulated vsize (Kb) 121772 [startup+870.053 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36156 0 0 0 86763 135 0 0 25 0 1 0 1740061749 120590336 27831 4294967295 134512640 135094434 3221221600 3221220212 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29441 27831 145 145 0 29296 0 [pid=20353] vsize: 117764 Current children cumulated CPU time (s) 868.98 Current children cumulated vsize (Kb) 121960 [startup+880.054 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36207 0 0 0 87762 135 0 0 25 0 1 0 1740061749 120795136 27882 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29491 27882 145 145 0 29346 0 [pid=20353] vsize: 117964 Current children cumulated CPU time (s) 878.97 Current children cumulated vsize (Kb) 122160 [startup+890.055 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36260 0 0 0 88760 136 0 0 25 0 1 0 1740061749 121012224 27935 4294967295 134512640 135094434 3221221600 3221220260 134553501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29544 27935 145 145 0 29399 0 [pid=20353] vsize: 118176 Current children cumulated CPU time (s) 888.96 Current children cumulated vsize (Kb) 122372 [startup+900.055 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36286 0 0 0 89760 137 0 0 25 0 1 0 1740061749 121114624 27961 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29569 27961 145 145 0 29424 0 [pid=20353] vsize: 118276 Current children cumulated CPU time (s) 898.97 Current children cumulated vsize (Kb) 122472 [startup+910.056 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36311 0 0 0 90760 137 0 0 25 0 1 0 1740061749 121217024 27986 4294967295 134512640 135094434 3221221600 3221220260 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29594 27986 145 145 0 29449 0 [pid=20353] vsize: 118376 Current children cumulated CPU time (s) 908.97 Current children cumulated vsize (Kb) 122572 [startup+920.056 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36328 0 0 0 91759 137 0 0 25 0 1 0 1740061749 121286656 28003 4294967295 134512640 135094434 3221221600 3221220224 134557655 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29611 28003 145 145 0 29466 0 [pid=20353] vsize: 118444 Current children cumulated CPU time (s) 918.96 Current children cumulated vsize (Kb) 122640 [startup+930.057 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36346 0 0 0 92759 138 0 0 25 0 1 0 1740061749 121421824 28021 4294967295 134512640 135094434 3221221600 3221220304 134559013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29644 28021 145 145 0 29499 0 [pid=20353] vsize: 118576 Current children cumulated CPU time (s) 928.97 Current children cumulated vsize (Kb) 122772 [startup+940.058 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36351 0 0 0 93759 138 0 0 25 0 1 0 1740061749 121442304 28026 4294967295 134512640 135094434 3221221600 3221220304 134558968 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29649 28026 145 145 0 29504 0 [pid=20353] vsize: 118596 Current children cumulated CPU time (s) 938.97 Current children cumulated vsize (Kb) 122792 [startup+950.058 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36355 0 0 0 94760 138 0 0 25 0 1 0 1740061749 121454592 28030 4294967295 134512640 135094434 3221221600 3221220260 134553450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29652 28030 145 145 0 29507 0 [pid=20353] vsize: 118608 Current children cumulated CPU time (s) 948.98 Current children cumulated vsize (Kb) 122804 [startup+960.059 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36373 0 0 0 95760 138 0 0 25 0 1 0 1740061749 121528320 28048 4294967295 134512640 135094434 3221221600 3221220260 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29670 28048 145 145 0 29525 0 [pid=20353] vsize: 118680 Current children cumulated CPU time (s) 958.98 Current children cumulated vsize (Kb) 122876 [startup+970.059 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36384 0 0 0 96760 138 0 0 25 0 1 0 1740061749 121569280 28059 4294967295 134512640 135094434 3221221600 3221220260 134553450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29680 28059 145 145 0 29535 0 [pid=20353] vsize: 118720 Current children cumulated CPU time (s) 968.98 Current children cumulated vsize (Kb) 122916 [startup+980.06 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36403 0 0 0 97759 138 0 0 25 0 1 0 1740061749 121638912 28078 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29697 28078 145 145 0 29552 0 [pid=20353] vsize: 118788 Current children cumulated CPU time (s) 978.97 Current children cumulated vsize (Kb) 122984 [startup+990.061 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36415 0 0 0 98759 139 0 0 25 0 1 0 1740061749 121688064 28090 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29709 28090 145 145 0 29564 0 [pid=20353] vsize: 118836 Current children cumulated CPU time (s) 988.98 Current children cumulated vsize (Kb) 123032 [startup+1000.06 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36430 0 0 0 99759 139 0 0 25 0 1 0 1740061749 121745408 28105 4294967295 134512640 135094434 3221221600 3221220260 134553489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29723 28105 145 145 0 29578 0 [pid=20353] vsize: 118892 Current children cumulated CPU time (s) 998.98 Current children cumulated vsize (Kb) 123088 [startup+1010.06 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36469 0 0 0 100758 139 0 0 25 0 1 0 1740061749 121876480 28144 4294967295 134512640 135094434 3221221600 3221220292 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29755 28144 145 145 0 29610 0 [pid=20353] vsize: 119020 Current children cumulated CPU time (s) 1008.97 Current children cumulated vsize (Kb) 123216 [startup+1020.06 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36475 0 0 0 101758 139 0 0 25 0 1 0 1740061749 121901056 28150 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29761 28150 145 145 0 29616 0 [pid=20353] vsize: 119044 Current children cumulated CPU time (s) 1018.97 Current children cumulated vsize (Kb) 123240 [startup+1030.06 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36488 0 0 0 102758 139 0 0 25 0 1 0 1740061749 121950208 28163 4294967295 134512640 135094434 3221221600 3221220260 134553501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29773 28163 145 145 0 29628 0 [pid=20353] vsize: 119092 Current children cumulated CPU time (s) 1028.97 Current children cumulated vsize (Kb) 123288 [startup+1040.06 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36511 0 0 0 103759 139 0 0 25 0 1 0 1740061749 122044416 28186 4294967295 134512640 135094434 3221221600 3221220260 134553444 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29796 28186 145 145 0 29651 0 [pid=20353] vsize: 119184 Current children cumulated CPU time (s) 1038.98 Current children cumulated vsize (Kb) 123380 [startup+1050.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36539 0 0 0 104758 140 0 0 25 0 1 0 1740061749 122155008 28214 4294967295 134512640 135094434 3221221600 3221220260 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29823 28214 145 145 0 29678 0 [pid=20353] vsize: 119292 Current children cumulated CPU time (s) 1048.98 Current children cumulated vsize (Kb) 123488 [startup+1060.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36554 0 0 0 105758 140 0 0 25 0 1 0 1740061749 122212352 28229 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29837 28229 145 145 0 29692 0 [pid=20353] vsize: 119348 Current children cumulated CPU time (s) 1058.98 Current children cumulated vsize (Kb) 123544 [startup+1070.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36569 0 0 0 106758 140 0 0 25 0 1 0 1740061749 122269696 28244 4294967295 134512640 135094434 3221221600 3221220260 134553494 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29851 28244 145 145 0 29706 0 [pid=20353] vsize: 119404 Current children cumulated CPU time (s) 1068.98 Current children cumulated vsize (Kb) 123600 [startup+1080.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36579 0 0 0 107758 140 0 0 25 0 1 0 1740061749 122310656 28254 4294967295 134512640 135094434 3221221600 3221220212 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29861 28254 145 145 0 29716 0 [pid=20353] vsize: 119444 Current children cumulated CPU time (s) 1078.98 Current children cumulated vsize (Kb) 123640 [startup+1090.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36592 0 0 0 108758 140 0 0 25 0 1 0 1740061749 122355712 28267 4294967295 134512640 135094434 3221221600 3221220272 134553523 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29872 28267 145 145 0 29727 0 [pid=20353] vsize: 119488 Current children cumulated CPU time (s) 1088.98 Current children cumulated vsize (Kb) 123684 [startup+1100.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36595 0 0 0 109758 140 0 0 25 0 1 0 1740061749 122368000 28270 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29875 28270 145 145 0 29730 0 [pid=20353] vsize: 119500 Current children cumulated CPU time (s) 1098.98 Current children cumulated vsize (Kb) 123696 [startup+1110.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36600 0 0 0 110758 140 0 0 25 0 1 0 1740061749 122388480 28275 4294967295 134512640 135094434 3221221600 3221220212 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29880 28275 145 145 0 29735 0 [pid=20353] vsize: 119520 Current children cumulated CPU time (s) 1108.98 Current children cumulated vsize (Kb) 123716 [startup+1120.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36621 0 0 0 111758 140 0 0 25 0 1 0 1740061749 122470400 28296 4294967295 134512640 135094434 3221221600 3221220212 134563064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29900 28296 145 145 0 29755 0 [pid=20353] vsize: 119600 Current children cumulated CPU time (s) 1118.98 Current children cumulated vsize (Kb) 123796 [startup+1130.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36649 0 0 0 112757 141 0 0 25 0 1 0 1740061749 122568704 28324 4294967295 134512640 135094434 3221221600 3221220260 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29924 28324 145 145 0 29779 0 [pid=20353] vsize: 119696 Current children cumulated CPU time (s) 1128.98 Current children cumulated vsize (Kb) 123892 [startup+1140.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36667 0 0 0 113757 141 0 0 25 0 1 0 1740061749 122626048 28342 4294967295 134512640 135094434 3221221600 3221220212 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20353/statm): 29938 28342 145 145 0 29793 0 [pid=20353] vsize: 119752 Current children cumulated CPU time (s) 1138.98 Current children cumulated vsize (Kb) 123948 [startup+1150.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36679 0 0 0 114756 141 0 0 25 0 1 0 1740061749 122671104 28354 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29949 28354 145 145 0 29804 0 [pid=20353] vsize: 119796 Current children cumulated CPU time (s) 1148.97 Current children cumulated vsize (Kb) 123992 [startup+1160.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36689 0 0 0 115757 141 0 0 25 0 1 0 1740061749 122712064 28364 4294967295 134512640 135094434 3221221600 3221220268 134553438 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 29959 28364 145 145 0 29814 0 [pid=20353] vsize: 119836 Current children cumulated CPU time (s) 1158.98 Current children cumulated vsize (Kb) 124032 [startup+1170.07 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36874 0 0 0 116754 143 0 0 25 0 1 0 1740061749 123457536 28549 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 30141 28549 145 145 0 29996 0 [pid=20353] vsize: 120564 Current children cumulated CPU time (s) 1168.97 Current children cumulated vsize (Kb) 124760 [startup+1180.08 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 37551 0 0 0 117745 146 0 0 25 0 1 0 1740061749 126328832 29226 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 30842 29226 145 145 0 30697 0 [pid=20353] vsize: 123368 Current children cumulated CPU time (s) 1178.91 Current children cumulated vsize (Kb) 127564 [startup+1190.08 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 38316 0 0 0 118733 151 0 0 25 0 1 0 1740061749 129433600 29991 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 31600 29991 145 145 0 31455 0 [pid=20353] vsize: 126400 Current children cumulated CPU time (s) 1188.84 Current children cumulated vsize (Kb) 130596 [startup+1200.08 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 38942 0 0 0 119722 156 0 0 25 0 1 0 1740061749 131960832 30617 4294967295 134512640 135094434 3221221600 3221220256 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 32217 30617 145 145 0 32072 0 [pid=20353] vsize: 128868 Current children cumulated CPU time (s) 1198.78 Current children cumulated vsize (Kb) 133064 [startup+1210.08 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 39508 0 0 0 120713 160 0 0 25 0 1 0 1740061749 134250496 31183 4294967295 134512640 135094434 3221221600 3221220272 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 32776 31183 145 145 0 32631 0 [pid=20353] vsize: 131104 Current children cumulated CPU time (s) 1208.73 Current children cumulated vsize (Kb) 135300 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 1.00 0.97 0.93 2/56 20353 Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0 [pid=20349] vsize: 4196 Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 39508 0 0 0 120713 160 0 0 25 0 1 0 1740061749 134250496 31183 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20353/statm): 32776 31183 145 145 0 32631 0 [pid=20353] vsize: 131104 Current children cumulated CPU time (s) 1208.73 Current children cumulated vsize (Kb) 135300 Sending SIGTERM to -20349 Sleeping 2 seconds One traced child (pid=20349) ended because it received signal 15 (SIGTERM) One traced child (pid=20353) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1208.79 CPU user time (s): 1207.13 CPU system time (s): 1.66175 CPU usage (%): 99.8887 Max. virtual memory (cumulated for all children) (Kb): 135300
ERROR: no interpretation found !