Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-boeing1.opb |
MD5SUM | 0ab24c5b60e18c0be832cc4080b37d61 |
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 | 6523 |
Biggest coefficient in the objective function | 24535000678400 |
Number of bits for the biggest coefficient in the objective function | 45 |
Sum of the numbers in the objective function | 1761916844753634 |
Number of bits of the sum of numbers in the objective function | 51 |
Biggest number in a constraint | 4102681610158080 |
Number of bits of the biggest number in a constraint | 52 |
Biggest sum of numbers in a constraint | 384599747612655519 |
Number of bits of the biggest sum of numbers | 59 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 8869 |
Total number of constraints | 593 |
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 | 593 |
Minimum length of a constraint | 11 |
Maximum length of a constraint | 6849 |
LAUNCH ON wulflinc18 THE 2005-09-18 20:12:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2758 boxname=wulflinc18 idbench=414 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 0ab24c5b60e18c0be832cc4080b37d61 /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-boeing1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-boeing1.opb IDLAUNCH: 2758 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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: 912144 kB Buffers: 35416 kB Cached: 52072 kB SwapCached: 844 kB Active: 68204 kB Inactive: 21916 kB HighTotal: 131008 kB HighFree: 76020 kB LowTotal: 903652 kB LowFree: 836124 kB SwapTotal: 2097892 kB SwapFree: 2096548 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5764 kB Slab: 26836 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:32:46 (client local time) WITH STATUS 0 IN 1200.07 SECONDS stats: 2758 7 1200.07 0
c Parsing PB file... c PARSE ERROR! [line 729] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 560 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: #######=# c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[ 652]---> BDD-cost: 16 c ---[ 651]---> BDD-cost: 16 c ---[ 650]---> BDD-cost: 15 c ---[ 649]---> BDD-cost: 15 c ---[ 648]---> BDD-cost: 16 c ---[ 647]---> BDD-cost: 16 c ---[ 646]---> BDD-cost: 11 c ---[ 645]---> BDD-cost: 11 c ---[ 644]---> BDD-cost: 11 c ---[ 643]---> BDD-cost: 11 c ---[ 642]---> BDD-cost: 11 c ---[ 641]---> BDD-cost: 11 c ---[ 640]---> BDD-cost: 12 c ---[ 639]---> BDD-cost: 12 c ---[ 638]---> BDD-cost: 12 c ---[ 637]---> BDD-cost: 12 c ---[ 636]---> BDD-cost: 12 c ---[ 635]---> BDD-cost: 12 c ---[ 634]---> BDD-cost: 11 c ---[ 633]---> BDD-cost: 10 c ---[ 632]---> BDD-cost: 11 c ---[ 631]---> BDD-cost: 11 c ---[ 630]---> BDD-cost: 11 c ---[ 629]---> BDD-cost: 11 c ---[ 600]---> BDD-cost: 12 c ---[ 599]---> BDD-cost: 12 c ---[ 598]---> BDD-cost: 12 c ---[ 597]---> BDD-cost: 12 c ---[ 596]---> BDD-cost: 12 c ---[ 595]---> BDD-cost: 12 c ---[ 594]---> BDD-cost: 12 c ---[ 593]---> BDD-cost: 12 c ---[ 592]---> BDD-cost: 12 c ---[ 591]---> BDD-cost: 12 c ---[ 590]---> BDD-cost: 12 c ---[ 589]---> BDD-cost: 12 c ---[ 588]---> BDD-cost: 12 c ---[ 587]---> BDD-cost: 12 c ---[ 586]---> BDD-cost: 12 c ---[ 585]---> BDD-cost: 12 c ---[ 584]---> BDD-cost: 12 c ---[ 583]---> BDD-cost: 12 c ---[ 582]---> BDD-cost: 12 c ---[ 581]---> BDD-cost: 12 c ---[ 558]---> BDD-cost: 10 c ---[ 555]---> BDD-cost: 10 c ---[ 554]---> BDD-cost: 10 c ---[ 553]---> BDD-cost: 10 c ---[ 552]---> BDD-cost: 10 c ---[ 551]---> BDD-cost: 10 c ---[ 550]---> BDD-cost: 10 c ---[ 549]---> BDD-cost: 10 c ---[ 548]---> BDD-cost: 10 c ---[ 547]---> BDD-cost: 10 c ---[ 546]---> BDD-cost: 12 c ---[ 545]---> BDD-cost: 12 c ---[ 544]---> BDD-cost: 12 c ---[ 543]---> BDD-cost: 12 c ---[ 542]---> BDD-cost: 12 c ---[ 541]---> BDD-cost: 12 c ---[ 540]---> BDD-cost: 12 c ---[ 539]---> BDD-cost: 12 c ---[ 538]---> BDD-cost: 12 c ---[ 537]---> BDD-cost: 12 c ---[ 536]---> BDD-cost: 12 c ---[ 535]---> BDD-cost: 12 c ---[ 534]---> BDD-cost: 12 c ---[ 533]---> BDD-cost: 12 c ---[ 532]---> BDD-cost: 12 c ---[ 531]---> BDD-cost: 12 c ---[ 530]---> BDD-cost: 12 c ---[ 529]---> BDD-cost: 12 c ---[ 528]---> BDD-cost: 13 c ---[ 527]---> BDD-cost: 13 c ---[ 524]---> BDD-cost: 13 c ---[ 523]---> BDD-cost: 13 c ---[ 522]---> BDD-cost: 13 c ---[ 521]---> BDD-cost: 14 c ---[ 520]---> BDD-cost: 14 c ---[ 519]---> BDD-cost: 14 c ---[ 518]---> BDD-cost: 14 c ---[ 517]---> BDD-cost: 14 c ---[ 516]---> BDD-cost: 14 c ---[ 515]---> BDD-cost: 11 c ---[ 514]---> BDD-cost: 11 c ---[ 513]---> BDD-cost: 11 c ---[ 512]---> BDD-cost: 11 c ---[ 511]---> BDD-cost: 11 c ---[ 510]---> BDD-cost: 11 c ---[ 509]---> BDD-cost: 11 c ---[ 508]---> BDD-cost: 10 c ---[ 507]---> BDD-cost: 10 c ---[ 506]---> BDD-cost: 10 c ---[ 505]---> BDD-cost: 12 c ---[ 504]---> BDD-cost: 12 c ---[ 503]---> BDD-cost: 12 c ---[ 502]---> BDD-cost: 14 c ---[ 501]---> BDD-cost: 14 c ---[ 500]---> BDD-cost: 14 c ---[ 499]---> BDD-cost: 14 c ---[ 498]---> BDD-cost: 14 c ---[ 497]---> BDD-cost: 14 c ---[ 496]---> Sorter-cost: 495 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 495]---> BDD-cost: 113 c ---[ 494]---> BDD-cost: 1 c ---[ 493]---> Sorter-cost: 1174 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 492]---> Sorter-cost: 1171 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 491]---> Sorter-cost: 1655 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 490]---> Sorter-cost: 1147 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 489]---> BDD-cost: 141 c ---[ 488]---> BDD-cost: 65 c ---[ 487]---> BDD-cost: 1 c ---[ 486]---> BDD-cost: 44 c ---[ 485]---> Sorter-cost: 1298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> BDD-cost: 48 c ---[ 483]---> BDD-cost: 3 c ---[ 482]---> Sorter-cost: 1768 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 481]---> Sorter-cost: 535 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 480]---> BDD-cost: 45 c ---[ 479]---> Sorter-cost: 1614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 477]---> BDD-cost: 3 c ---[ 476]---> Sorter-cost: 1549 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 475]---> BDD-cost: 3 c ---[ 474]---> Sorter-cost: 877 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 473]---> BDD-cost: 55 c ---[ 472]---> BDD-cost: 117 c ---[ 471]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 470]---> Adder-cost: 468 maxlim: 879611 bits: 21/20 c ---[ 469]---> Sorter-cost: 3692 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 468]---> Sorter-cost: 535 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 467]---> Sorter-cost: 572 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 466]---> Sorter-cost: 976 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 465]---> Sorter-cost: 1318 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 464]---> BDD-cost: 142 c ---[ 463]---> BDD-cost: 45 c ---[ 462]---> Sorter-cost: 1419 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 461]---> Sorter-cost: 1336 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 460]---> BDD-cost: 47 c ---[ 459]---> Sorter-cost: 1595 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 458]---> BDD-cost: 139 c ---[ 457]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 456]---> BDD-cost: 4 c ---[ 455]---> Sorter-cost: 3517 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 454]---> Adder-cost: 299 maxlim: 100343 bits: 18/17 c ---[ 453]---> Adder-cost: 331 maxlim: 239607 bits: 19/18 c ---[ 452]---> Adder-cost: 456 maxlim: 1060858 bits: 22/21 c ---[ 450]---> BDD-cost: 64 c ---[ 449]---> Sorter-cost: 613 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 448]---> Sorter-cost: 761 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 447]---> BDD-cost: 1 c ---[ 446]---> BDD-cost: 2 c ---[ 445]---> Sorter-cost: 841 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 444]---> BDD-cost: 2 c ---[ 443]---> BDD-cost: 4 c ---[ 442]---> Sorter-cost: 1658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 441]---> Sorter-cost: 1114 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 440]---> Sorter-cost: 1321 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 439]---> Sorter-cost: 1275 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 438]---> Sorter-cost: 1332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 435]---> BDD-cost: 12 c ---[ 434]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 433]---> Sorter-cost: 293 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 432]---> BDD-cost: 11 c ---[ 431]---> BDD-cost: 58 c ---[ 430]---> Sorter-cost: 972 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 429]---> Sorter-cost: 1002 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 428]---> BDD-cost: 48 c ---[ 427]---> BDD-cost: 53 c ---[ 426]---> Sorter-cost: 1393 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 425]---> Sorter-cost: 947 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 424]---> Sorter-cost: 339 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 423]---> BDD-cost: 83 c ---[ 422]---> BDD-cost: 11 c ---[ 421]---> BDD-cost: 10 c ---[ 420]---> BDD-cost: 68 c ---[ 419]---> BDD-cost: 10 c ---[ 418]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 417]---> BDD-cost: 49 c ---[ 416]---> BDD-cost: 10 c ---[ 415]---> BDD-cost: 11 c ---[ 414]---> BDD-cost: 13 c ---[ 413]---> Sorter-cost: 1534 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 412]---> BDD-cost: 58 c ---[ 411]---> Sorter-cost: 390 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 410]---> BDD-cost: 68 c ---[ 409]---> BDD-cost: 48 c ---[ 408]---> Sorter-cost: 1388 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 407]---> Sorter-cost: 341 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 406]---> BDD-cost: 13 c ---[ 405]-
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/6228/stat): 6228 (minisat+_script) R 6227 6228 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844007712 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/6228/statm): 174 3 169 147 0 27 0 [pid=6228] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=6229 New process pid=6230 New process pid=6231 execve syscall for /bin/sed executable One traced child (pid=6230) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=6231) exited with status: 0 One traced child (pid=6229) exited with status: 0 New process pid=6232 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-boeing1.opb One traced child (pid=6232) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=6233 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-boeing1.opb [startup+10.0037 s] Raw data (loadavg): 0.94 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 2208 0 3 0 924 12 0 0 25 0 1 0 1844007746 8695808 1872 4294967295 134512640 135167914 3221224448 3221222272 134696613 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 2123 1872 162 162 0 1961 0 [pid=6233] vsize: 8492 Current children cumulated CPU time (s) 9.62 Current children cumulated vsize (Kb) 10620 [startup+20.0047 s] Raw data (loadavg): 0.95 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 6843 0 3 0 1884 32 0 0 25 0 1 0 1844007746 25088000 5804 4294967295 134512640 135167914 3221224448 3221138704 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 6125 5804 162 162 0 5963 0 [pid=6233] vsize: 24500 Current children cumulated CPU time (s) 19.42 Current children cumulated vsize (Kb) 26628 [startup+30.0056 s] Raw data (loadavg): 0.95 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 12616 0 3 0 2833 58 0 0 25 0 1 0 1844007746 46034944 10918 4294967295 134512640 135167914 3221224448 3221138784 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 11239 10918 162 162 0 11077 0 [pid=6233] vsize: 44956 Current children cumulated CPU time (s) 29.17 Current children cumulated vsize (Kb) 47084 [startup+40.0065 s] Raw data (loadavg): 0.96 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 19296 0 3 0 3783 84 0 0 25 0 1 0 1844007746 67993600 16280 4294967295 134512640 135167914 3221224448 3221137952 134845321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 16600 16280 162 162 0 16438 0 [pid=6233] vsize: 66400 Current children cumulated CPU time (s) 38.93 Current children cumulated vsize (Kb) 68528 [startup+50.0085 s] Raw data (loadavg): 0.97 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 24712 0 3 0 4732 108 0 0 25 0 1 0 1844007746 108208128 21696 4294967295 134512640 135167914 3221224448 3221139040 134625368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 26418 21696 162 162 0 26256 0 [pid=6233] vsize: 105672 Current children cumulated CPU time (s) 48.66 Current children cumulated vsize (Kb) 107800 [startup+60.0094 s] Raw data (loadavg): 0.97 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 32531 0 3 0 5680 136 0 0 25 0 1 0 1844007746 111403008 26878 4294967295 134512640 135167914 3221224448 3221142128 134845881 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 27198 26878 162 162 0 27036 0 [pid=6233] vsize: 108792 Current children cumulated CPU time (s) 58.42 Current children cumulated vsize (Kb) 110920 [startup+70.0103 s] Raw data (loadavg): 0.97 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 36802 0 3 0 6633 158 0 0 25 0 1 0 1844007746 128897024 31149 4294967295 134512640 135167914 3221224448 3221138272 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 31469 31149 162 162 0 31307 0 [pid=6233] vsize: 125876 Current children cumulated CPU time (s) 68.17 Current children cumulated vsize (Kb) 128004 [startup+80.0112 s] Raw data (loadavg): 0.98 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 41061 0 3 0 7588 178 0 0 25 0 1 0 1844007746 146341888 35408 4294967295 134512640 135167914 3221224448 3221139860 134697403 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 35728 35408 162 162 0 35566 0 [pid=6233] vsize: 142912 Current children cumulated CPU time (s) 77.92 Current children cumulated vsize (Kb) 145040 [startup+90.0122 s] Raw data (loadavg): 0.98 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 52641 0 3 0 8526 213 0 0 25 0 1 0 1844007746 205725696 46988 4294967295 134512640 135167914 3221224448 3221139712 134625368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 50226 46988 162 162 0 50064 0 [pid=6233] vsize: 200904 Current children cumulated CPU time (s) 87.65 Current children cumulated vsize (Kb) 203032 [startup+100.013 s] Raw data (loadavg): 0.98 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 58006 0 3 0 9492 232 0 0 25 0 1 0 1844007746 194146304 47080 4294967295 134512640 135167914 3221224448 3221141936 134849066 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 47399 47080 162 162 0 47237 0 [pid=6233] vsize: 189596 Current children cumulated CPU time (s) 97.5 Current children cumulated vsize (Kb) 191724 [startup+110.014 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 62112 0 3 0 10448 252 0 0 25 0 1 0 1844007746 210964480 51186 4294967295 134512640 135167914 3221224448 3221139004 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 51505 51186 162 162 0 51343 0 [pid=6233] vsize: 206020 Current children cumulated CPU time (s) 107.26 Current children cumulated vsize (Kb) 208148 [startup+120.015 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 66004 0 3 0 11406 267 0 0 25 0 1 0 1844007746 226902016 55078 4294967295 134512640 135167914 3221224448 3221138288 134623813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 55396 55078 162 162 0 55234 0 [pid=6233] vsize: 221584 Current children cumulated CPU time (s) 116.99 Current children cumulated vsize (Kb) 223712 [startup+130.016 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 70115 0 3 0 12358 286 0 0 18 0 1 0 1844007746 243740672 59189 4294967295 134512640 135167914 3221224448 3221141616 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 59507 59189 162 162 0 59345 0 [pid=6233] vsize: 238028 Current children cumulated CPU time (s) 126.7 Current children cumulated vsize (Kb) 240156 [startup+140.017 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 73917 0 3 0 13321 303 0 0 25 0 1 0 1844007746 259313664 62991 4294967295 134512640 135167914 3221224448 3221139840 134844703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 63309 62991 162 162 0 63147 0 [pid=6233] vsize: 253236 Current children cumulated CPU time (s) 136.5 Current children cumulated vsize (Kb) 255364 [startup+150.019 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 77997 0 3 0 14278 321 0 0 25 0 1 0 1844007746 276017152 67071 4294967295 134512640 135167914 3221224448 3221140128 134694444 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 67387 67071 162 162 0 67225 0 [pid=6233] vsize: 269548 Current children cumulated CPU time (s) 146.25 Current children cumulated vsize (Kb) 271676 [startup+160.02 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 81884 0 3 0 15239 337 0 0 25 0 1 0 1844007746 291938304 70958 4294967295 134512640 135167914 3221224448 3221139408 134623813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 71274 70958 162 162 0 71112 0 [pid=6233] vsize: 285096 Current children cumulated CPU time (s) 156.02 Current children cumulated vsize (Kb) 287224 [startup+170.02 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 85527 0 3 0 16201 352 0 0 25 0 1 0 1844007746 306855936 74601 4294967295 134512640 135167914 3221224448 3221140304 134623813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 74916 74601 162 162 0 74754 0 [pid=6233] vsize: 299664 Current children cumulated CPU time (s) 165.79 Current children cumulated vsize (Kb) 301792 [startup+180.02 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 108458 0 3 0 17134 408 0 0 25 0 1 0 1844007746 400781312 97532 4294967295 134512640 135167914 3221224448 3221138672 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 97847 97532 162 162 0 97685 0 [pid=6233] vsize: 391388 Current children cumulated CPU time (s) 175.68 Current children cumulated vsize (Kb) 393516 [startup+190.021 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 111015 0 3 0 18106 421 0 0 25 0 1 0 1844007746 368058368 89543 4294967295 134512640 135167914 3221224448 3221142624 134847359 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 89858 89543 162 162 0 89696 0 [pid=6233] vsize: 359432 Current children cumulated CPU time (s) 185.53 Current children cumulated vsize (Kb) 361560 [startup+200.022 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 114867 0 3 0 19065 439 0 0 25 0 1 0 1844007746 383836160 93395 4294967295 134512640 135167914 3221224448 3221140080 134843420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 93710 93395 162 162 0 93548 0 [pid=6233] vsize: 374840 Current children cumulated CPU time (s) 195.3 Current children cumulated vsize (Kb) 376968 [startup+210.023 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 118617 0 3 0 20025 456 0 0 25 0 1 0 1844007746 399192064 97145 4294967295 134512640 135167914 3221224448 3221139392 134623794 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 97459 97145 162 162 0 97297 0 [pid=6233] vsize: 389836 Current children cumulated CPU time (s) 205.07 Current children cumulated vsize (Kb) 391964 [startup+220.026 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 122195 0 3 0 20985 472 0 0 25 0 1 0 1844007746 413847552 100723 4294967295 134512640 135167914 3221224448 3221138976 134695806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 101037 100723 162 162 0 100875 0 [pid=6233] vsize: 404148 Current children cumulated CPU time (s) 214.83 Current children cumulated vsize (Kb) 406276 [startup+230.027 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 125612 0 3 0 21948 486 0 0 25 0 1 0 1844007746 427835392 104140 4294967295 134512640 135167914 3221224448 3221139744 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 104452 104140 162 162 0 104290 0 [pid=6233] vsize: 417808 Current children cumulated CPU time (s) 224.6 Current children cumulated vsize (Kb) 419936 [startup+240.028 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 129679 0 3 0 22907 504 0 0 25 0 1 0 1844007746 443817984 108042 4294967295 134512640 135167914 3221224448 3221138944 134624024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 108354 108042 162 162 0 108192 0 [pid=6233] vsize: 433416 Current children cumulated CPU time (s) 234.37 Current children cumulated vsize (Kb) 435544 [startup+250.029 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 133572 0 3 0 23865 521 0 0 25 0 1 0 1844007746 459763712 111935 4294967295 134512640 135167914 3221224448 3221141040 134693563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 112247 111935 162 162 0 112085 0 [pid=6233] vsize: 448988 Current children cumulated CPU time (s) 244.12 Current children cumulated vsize (Kb) 451116 [startup+260.03 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 137308 0 3 0 24825 538 0 0 25 0 1 0 1844007746 475062272 115671 4294967295 134512640 135167914 3221224448 3221143580 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 115982 115671 162 162 0 115820 0 [pid=6233] vsize: 463928 Current children cumulated CPU time (s) 253.89 Current children cumulated vsize (Kb) 466056 [startup+270.03 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 141014 0 3 0 25787 556 0 0 25 0 1 0 1844007746 490237952 119377 4294967295 134512640 135167914 3221224448 3221140976 134623813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 119687 119377 162 162 0 119525 0 [pid=6233] vsize: 478748 Current children cumulated CPU time (s) 263.69 Current children cumulated vsize (Kb) 480876 [startup+280.031 s] Raw data (loadavg): 0.99 0.98 0.96 1/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) T 6228 6228 31027 0 -1 0 144478 0 3 0 26751 571 0 0 25 0 1 0 1844007746 504426496 122841 4294967295 134512640 135167914 3221224448 3221139548 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6233/statm): 123151 122841 162 162 0 122989 0 [pid=6233] vsize: 492604 Current children cumulated CPU time (s) 273.48 Current children cumulated vsize (Kb) 494732 [startup+290.032 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 147800 0 3 0 27714 586 0 0 25 0 1 0 1844007746 518029312 126163 4294967295 134512640 135167914 3221224448 3221142336 134522502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 126472 126163 162 162 0 126310 0 [pid=6233] vsize: 505888 Current children cumulated CPU time (s) 283.26 Current children cumulated vsize (Kb) 508016 [startup+300.033 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 151045 0 3 0 28678 601 0 0 25 0 1 0 1844007746 531316736 129408 4294967295 134512640 135167914 3221224448 3221139120 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 129716 129408 162 162 0 129554 0 [pid=6233] vsize: 518864 Current children cumulated CPU time (s) 293.05 Current children cumulated vsize (Kb) 520992 [startup+310.034 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 155046 0 3 0 29636 619 0 0 25 0 1 0 1844007746 547700736 133409 4294967295 134512640 135167914 3221224448 3221141424 134623803 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 133716 133409 162 162 0 133554 0 [pid=6233] vsize: 534864 Current children cumulated CPU time (s) 302.81 Current children cumulated vsize (Kb) 536992 [startup+320.034 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 158880 0 3 0 30595 636 0 0 25 0 1 0 1844007746 563400704 137243 4294967295 134512640 135167914 3221224448 3221141692 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 137549 137243 162 162 0 137387 0 [pid=6233] vsize: 550196 Current children cumulated CPU time (s) 312.57 Current children cumulated vsize (Kb) 552324 [startup+330.035 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) T 6228 6228 31027 0 -1 0 162572 0 3 0 31558 652 0 0 25 0 1 0 1844007746 578519040 140935 4294967295 134512640 135167914 3221224448 3221139452 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/6233/statm): 141240 140935 162 162 0 141078 0 [pid=6233] vsize: 564960 Current children cumulated CPU time (s) 322.36 Current children cumulated vsize (Kb) 567088 [startup+340.035 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 166058 0 3 0 32523 665 0 0 25 0 1 0 1844007746 592793600 144421 4294967295 134512640 135167914 3221224448 3221139356 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 144725 144421 162 162 0 144563 0 [pid=6233] vsize: 578900 Current children cumulated CPU time (s) 332.14 Current children cumulated vsize (Kb) 581028 [startup+350.036 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 169323 0 3 0 33490 679 0 0 25 0 1 0 1844007746 606162944 147686 4294967295 134512640 135167914 3221224448 3221140368 134849108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 147989 147686 162 162 0 147827 0 [pid=6233] vsize: 591956 Current children cumulated CPU time (s) 341.95 Current children cumulated vsize (Kb) 594084 [startup+360.037 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 192536 0 3 0 34412 738 0 0 25 0 1 0 1844007746 791609344 170899 4294967295 134512640 135167914 3221224448 3221141504 134625368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 193264 170899 162 162 0 193102 0 [pid=6233] vsize: 773056 Current children cumulated CPU time (s) 351.76 Current children cumulated vsize (Kb) 775184 [startup+370.038 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 214599 0 3 0 35364 785 0 0 25 0 1 0 1844007746 791609344 192962 4294967295 134512640 135167914 3221224448 3221141436 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 193264 192962 162 162 0 193102 0 [pid=6233] vsize: 773056 Current children cumulated CPU time (s) 361.75 Current children cumulated vsize (Kb) 775184 [startup+380.039 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 215623 0 3 0 36349 794 0 0 25 0 1 0 1844007746 709410816 172895 4294967295 134512640 135167914 3221224448 3221140976 134623803 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 173196 172895 162 162 0 173034 0 [pid=6233] vsize: 692784 Current children cumulated CPU time (s) 371.69 Current children cumulated vsize (Kb) 694912 [startup+390.04 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 219482 0 3 0 37309 808 0 0 25 0 1 0 1844007746 725213184 176754 4294967295 134512640 135167914 3221224448 3221139136 134849179 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 177054 176754 162 162 0 176892 0 [pid=6233] vsize: 708216 Current children cumulated CPU time (s) 381.43 Current children cumulated vsize (Kb) 710344 [startup+400.041 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 223313 0 3 0 38270 824 0 0 25 0 1 0 1844007746 740900864 180585 4294967295 134512640 135167914 3221224448 3221141088 134844718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 180884 180585 162 162 0 180722 0 [pid=6233] vsize: 723536 Current children cumulated CPU time (s) 391.2 Current children cumulated vsize (Kb) 725664 [startup+410.042 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 226936 0 3 0 39234 837 0 0 25 0 1 0 1844007746 755736576 184208 4294967295 134512640 135167914 3221224448 3221141180 134516612 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 184506 184208 162 162 0 184344 0 [pid=6233] vsize: 738024 Current children cumulated CPU time (s) 400.97 Current children cumulated vsize (Kb) 740152 [startup+420.042 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 230414 0 3 0 40194 853 0 0 25 0 1 0 1844007746 769974272 187686 4294967295 134512640 135167914 3221224448 3221139904 134843153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 187982 187686 162 162 0 187820 0 [pid=6233] vsize: 751928 Current children cumulated CPU time (s) 410.73 Current children cumulated vsize (Kb) 754056 [startup+430.043 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 233926 0 3 0 41159 867 0 0 25 0 1 0 1844007746 784355328 191198 4294967295 134512640 135167914 3221224448 3221140192 134843026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 191493 191198 162 162 0 191331 0 [pid=6233] vsize: 765972 Current children cumulated CPU time (s) 420.52 Current children cumulated vsize (Kb) 768100 [startup+440.043 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 237155 0 3 0 42124 881 0 0 25 0 1 0 1844007746 797577216 194427 4294967295 134512640 135167914 3221224448 3221139696 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 194721 194427 162 162 0 194559 0 [pid=6233] vsize: 778884 Current children cumulated CPU time (s) 430.31 Current children cumulated vsize (Kb) 781012 [startup+450.044 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 240282 0 3 0 43094 895 0 0 25 0 1 0 1844007746 810381312 197554 4294967295 134512640 135167914 3221224448 3221141264 134843030 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 197847 197554 162 162 0 197685 0 [pid=6233] vsize: 791388 Current children cumulated CPU time (s) 440.15 Current children cumulated vsize (Kb) 793516 [startup+460.045 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 243208 0 3 0 44065 907 0 0 25 0 1 0 1844007746 822362112 200480 4294967295 134512640 135167914 3221224448 3221139344 134854320 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 200772 200480 162 162 0 200610 0 [pid=6233] vsize: 803088 Current children cumulated CPU time (s) 449.98 Current children cumulated vsize (Kb) 805216 [startup+470.045 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 45052 912 0 0 25 0 1 0 1844007746 827047936 201626 4294967295 134512640 135167914 3221224448 3221223232 134623599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 201916 201626 162 162 0 201754 0 [pid=6233] vsize: 807664 Current children cumulated CPU time (s) 459.9 Current children cumulated vsize (Kb) 809792 [startup+480.047 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 46044 920 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221222984 134846910 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 469.9 Current children cumulated vsize (Kb) 641064 [startup+490.048 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 47044 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221222984 134846907 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 479.91 Current children cumulated vsize (Kb) 641064 [startup+500.05 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 48043 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218924 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 489.9 Current children cumulated vsize (Kb) 641064 [startup+510.051 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 49044 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219236 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 499.91 Current children cumulated vsize (Kb) 641064 [startup+520.052 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 50043 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219344 134849071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 509.9 Current children cumulated vsize (Kb) 641064 [startup+530.053 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 51044 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219004 134693585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 519.91 Current children cumulated vsize (Kb) 641064 [startup+540.054 s] Raw data (loadavg): 0.99 0.98 0.96 3/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 52043 922 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218800 134843015 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 529.91 Current children cumulated vsize (Kb) 641064 [startup+550.055 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 53043 922 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218988 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 539.91 Current children cumulated vsize (Kb) 641064 [startup+560.056 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 54043 922 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219072 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 549.91 Current children cumulated vsize (Kb) 641064 [startup+570.057 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 55043 923 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219460 134843000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 559.92 Current children cumulated vsize (Kb) 641064 [startup+580.057 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 56043 923 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219516 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 569.92 Current children cumulated vsize (Kb) 641064 [startup+590.058 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 57043 923 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219200 134845913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 579.92 Current children cumulated vsize (Kb) 641064 [startup+600.059 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 58042 923 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219520 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 589.91 Current children cumulated vsize (Kb) 641064 [startup+610.06 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 59042 924 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218912 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 599.92 Current children cumulated vsize (Kb) 641064 [startup+620.061 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 60042 924 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219328 134522767 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 609.92 Current children cumulated vsize (Kb) 641064 [startup+630.062 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 61042 924 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219296 134693573 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 619.92 Current children cumulated vsize (Kb) 641064 [startup+640.063 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 62041 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134845890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 629.92 Current children cumulated vsize (Kb) 641064 [startup+650.064 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 63042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219072 134718501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 639.93 Current children cumulated vsize (Kb) 641064 [startup+660.065 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 64041 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219616 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 649.92 Current children cumulated vsize (Kb) 641064 [startup+670.066 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 65042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219264 134696738 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 659.93 Current children cumulated vsize (Kb) 641064 [startup+680.067 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 66042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219276 134723246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 669.93 Current children cumulated vsize (Kb) 641064 [startup+690.068 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 67042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218800 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 679.93 Current children cumulated vsize (Kb) 641064 [startup+700.068 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 68042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219152 134694528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 689.93 Current children cumulated vsize (Kb) 641064 [startup+710.069 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 69042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218800 134694511 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 699.93 Current children cumulated vsize (Kb) 641064 [startup+720.069 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 70042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219516 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 709.93 Current children cumulated vsize (Kb) 641064 [startup+730.07 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 71043 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218976 134843068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 719.94 Current children cumulated vsize (Kb) 641064 [startup+740.07 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 72043 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219264 134844641 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 729.94 Current children cumulated vsize (Kb) 641064 [startup+750.072 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 73043 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219884 134693585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 739.94 Current children cumulated vsize (Kb) 641064 [startup+760.073 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 74043 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218784 134522821 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 749.94 Current children cumulated vsize (Kb) 641064 [startup+770.073 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 75044 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219308 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 759.95 Current children cumulated vsize (Kb) 641064 [startup+780.074 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 76043 926 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219440 134696366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 769.95 Current children cumulated vsize (Kb) 641064 [startup+790.075 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 77044 926 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218768 134845881 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 779.96 Current children cumulated vsize (Kb) 641064 [startup+800.076 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 78044 926 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218736 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 789.96 Current children cumulated vsize (Kb) 641064 [startup+810.077 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 79043 927 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219968 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 799.96 Current children cumulated vsize (Kb) 641064 [startup+820.08 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 80043 927 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219264 134844720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 809.96 Current children cumulated vsize (Kb) 641064 [startup+830.081 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 81043 928 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134696304 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 819.97 Current children cumulated vsize (Kb) 641064 [startup+840.081 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 82043 928 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218720 134845901 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 829.97 Current children cumulated vsize (Kb) 641064 [startup+850.083 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 83043 928 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218836 134629267 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 839.97 Current children cumulated vsize (Kb) 641064 [startup+860.084 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 84043 928 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219616 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 849.97 Current children cumulated vsize (Kb) 641064 [startup+870.084 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 85043 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219200 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 859.98 Current children cumulated vsize (Kb) 641064 [startup+880.085 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 86043 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218764 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 869.98 Current children cumulated vsize (Kb) 641064 [startup+890.086 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 87043 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134845930 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 879.98 Current children cumulated vsize (Kb) 641064 [startup+900.087 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 88043 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219336 134722513 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 889.98 Current children cumulated vsize (Kb) 641064 [startup+910.088 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 89044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218928 134843113 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 899.99 Current children cumulated vsize (Kb) 641064 [startup+920.089 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 90044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218992 134693570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 909.99 Current children cumulated vsize (Kb) 641064 [startup+930.09 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 91044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218828 134696788 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 919.99 Current children cumulated vsize (Kb) 641064 [startup+940.091 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 92044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219276 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 929.99 Current children cumulated vsize (Kb) 641064 [startup+950.092 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 93044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219072 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 939.99 Current children cumulated vsize (Kb) 641064 [startup+960.093 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 94043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219728 134629322 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 949.99 Current children cumulated vsize (Kb) 641064 [startup+970.093 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 95043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219168 134694338 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 959.99 Current children cumulated vsize (Kb) 641064 [startup+980.094 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 96043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219500 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 969.99 Current children cumulated vsize (Kb) 641064 [startup+990.095 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 97043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219120 134844637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 979.99 Current children cumulated vsize (Kb) 641064 [startup+1000.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 98042 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134844676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 989.98 Current children cumulated vsize (Kb) 641064 [startup+1010.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 99042 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219004 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 999.98 Current children cumulated vsize (Kb) 641064 [startup+1020.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 100042 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219120 134720470 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1009.98 Current children cumulated vsize (Kb) 641064 [startup+1030.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 101043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219344 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1019.99 Current children cumulated vsize (Kb) 641064 [startup+1040.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 102042 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218988 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1029.98 Current children cumulated vsize (Kb) 641064 [startup+1050.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 103043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219148 134722208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1039.99 Current children cumulated vsize (Kb) 641064 [startup+1060.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 104043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218800 134522296 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1049.99 Current children cumulated vsize (Kb) 641064 [startup+1070.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 105043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218976 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1059.99 Current children cumulated vsize (Kb) 641064 [startup+1080.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 106043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219168 134694351 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1069.99 Current children cumulated vsize (Kb) 641064 [startup+1090.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 107043 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219440 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1080 Current children cumulated vsize (Kb) 641064 [startup+1100.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 108044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219000 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1090.01 Current children cumulated vsize (Kb) 641064 [startup+1110.1 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 109044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218956 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1100.01 Current children cumulated vsize (Kb) 641064 [startup+1120.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 110044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219328 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1110.01 Current children cumulated vsize (Kb) 641064 [startup+1130.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 111044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219148 134695248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1120.01 Current children cumulated vsize (Kb) 641064 [startup+1140.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 112045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219856 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1130.02 Current children cumulated vsize (Kb) 641064 [startup+1150.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 113044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218848 134629382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1140.01 Current children cumulated vsize (Kb) 641064 [startup+1160.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 114045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219632 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1150.02 Current children cumulated vsize (Kb) 641064 [startup+1170.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 115045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219704 134696787 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1160.02 Current children cumulated vsize (Kb) 641064 [startup+1180.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 116045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219832 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1170.02 Current children cumulated vsize (Kb) 641064 [startup+1190.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 117045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219452 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1180.02 Current children cumulated vsize (Kb) 641064 [startup+1200.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 118046 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134696304 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1190.03 Current children cumulated vsize (Kb) 641064 [startup+1210.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 119046 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219692 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1200.03 Current children cumulated vsize (Kb) 641064 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6233 Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6228/statm): 532 234 485 147 0 385 0 [pid=6228] vsize: 2128 Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 119046 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219584 134844672 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0 [pid=6233] vsize: 638936 Current children cumulated CPU time (s) 1200.03 Current children cumulated vsize (Kb) 641064 Sending SIGTERM to -6228 Sleeping 2 seconds One traced child (pid=6228) ended because it received signal 15 (SIGTERM) One traced child (pid=6233) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.41 CPU time (s): 1200.07 CPU user time (s): 1190.46 CPU system time (s): 9.60754 CPU usage (%): 99.1461 Max. virtual memory (cumulated for all children) (Kb): 809792
ERROR: no interpretation found !