Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-tuff.opb |
MD5SUM | 1a92e09c7ec9849a6357a8d28097331d |
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 | 90 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 3221225469 |
Number of bits of the sum of numbers in the objective function | 32 |
Biggest number in a constraint | 6170044790734848 |
Number of bits of the biggest number in a constraint | 53 |
Biggest sum of numbers in a constraint | 1104744513968841438 |
Number of bits of the biggest sum of numbers | 60 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 17153 |
Total number of constraints | 320 |
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 | 320 |
Minimum length of a constraint | 11 |
Maximum length of a constraint | 3360 |
LAUNCH ON wulflinc17 THE 2005-09-18 20:38:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2826 boxname=wulflinc17 idbench=482 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1a92e09c7ec9849a6357a8d28097331d /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-tuff.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-tuff.opb IDLAUNCH: 2826 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 915640 kB Buffers: 31848 kB Cached: 60048 kB SwapCached: 516 kB Active: 36736 kB Inactive: 57612 kB HighTotal: 131008 kB HighFree: 67032 kB LowTotal: 903652 kB LowFree: 848608 kB SwapTotal: 2097892 kB SwapFree: 2096672 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5680 kB Slab: 19036 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:58:35 (client local time) WITH STATUS 0 IN 1208.74 SECONDS stats: 2826 7 1208.74 0
c Parsing PB file... c PARSE ERROR! [line 632] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 553 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): sss c ---[ 555]---> BDD-cost: 13 c ---[ 554]---> BDD-cost: 13 c ---[ 553]---> BDD-cost: 15 c ---[ 552]---> BDD-cost: 13 c ---[ 551]---> BDD-cost: 14 c ---[ 550]---> BDD-cost: 17 c ---[ 549]---> BDD-cost: 14 c ---[ 548]---> BDD-cost: 14 c ---[ 547]---> BDD-cost: 11 c ---[ 546]---> BDD-cost: 12 c ---[ 542]---> BDD-cost: 14 c ---[ 537]---> BDD-cost: 15 c ---[ 536]---> BDD-cost: 18 c ---[ 534]---> BDD-cost: 15 c ---[ 533]---> BDD-cost: 11 c ---[ 532]---> BDD-cost: 13 c ---[ 531]---> BDD-cost: 13 c ---[ 530]---> BDD-cost: 10 c ---[ 528]---> Sorter-cost: 3586 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 526]---> Sorter-cost: 4073 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 522]---> Sorter-cost: 2856 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 c ---[ 520]---> BDD-cost: 860 c ---[ 518]---> Sorter-cost: 7141 Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 514]---> Sorter-cost: 6165 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 512]---> Sorter-cost: 817 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 510]---> Sorter-cost: 947 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 506]---> Sorter-cost: 947 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 504]---> Sorter-cost: 947 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 502]---> BDD-cost: 52 c ---[ 500]---> BDD-cost: 63 c ---[ 496]---> BDD-cost: 63 c ---[ 494]---> BDD-cost: 218 c ---[ 492]---> BDD-cost: 485 c ---[ 488]---> Sorter-cost: 5871 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 c ---[ 486]---> BDD-cost: 52 c ---[ 484]---> BDD-cost: 63 c ---[ 480]---> BDD-cost: 63 c ---[ 478]---> BDD-cost: 63 c ---[ 476]---> Adder-cost: 661 maxlim: 18284358 bits: 26/25 c ---[ 474]---> Sorter-cost: 1263 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 472]---> Sorter-cost: 508 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 470]---> BDD-cost: 146 c ---[ 468]---> BDD-cost: 48 c ---[ 464]---> BDD-cost: 48 c ---[ 462]---> BDD-cost: 48 c ---[ 460]---> BDD-cost: 202 c ---[ 456]---> BDD-cost: 48 c ---[ 452]---> BDD-cost: 48 c ---[ 450]---> Adder-cost: 1249 maxlim: 71234362 bits: 28/27 c ---[ 448]---> Adder-cost: 408 maxlim: 2801493 bits: 23/22 c ---[ 444]---> Adder-cost: 1534 maxlim: 377549754 bits: 30/29 c ---[ 442]---> BDD-cost: 1124 c ---[ 440]---> Sorter-cost: 3387 Base: 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 438]---> Sorter-cost: 499 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 436]---> BDD-cost: 37 c ---[ 434]---> BDD-cost: 37 c ---[ 432]---> BDD-cost: 55 c ---[ 430]---> Sorter-cost: 4596 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 428]---> Sorter-cost: 663 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 426]---> Sorter-cost: 4744 Base: 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 c ---[ 424]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 422]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 420]---> Sorter-cost: 663 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 418]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 416]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 414]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 412]---> Sorter-cost: 586 Base: 2 2 2 2 2 2 2 2 2 2 2 2
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/27535/stat): 27535 (minisat+_script) R 27534 27535 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844221203 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27535/statm): 174 3 169 147 0 27 0 [pid=27535] 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=27536 New process pid=27537 New process pid=27538 execve syscall for /bin/sed executable One traced child (pid=27537) 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=27538) exited with status: 0 One traced child (pid=27536) exited with status: 0 New process pid=27539 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-tuff.opb One traced child (pid=27539) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=27540 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-tuff.opb [startup+10.0031 s] Raw data (loadavg): 0.89 0.94 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 3401 0 0 0 948 19 0 0 25 0 1 0 1844221215 13135872 2877 4294967295 134512640 135167914 3221224448 3221222244 134845880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 3207 2877 162 162 0 3045 0 [pid=27540] vsize: 12828 Current children cumulated CPU time (s) 9.73 Current children cumulated vsize (Kb) 14956 [startup+20.0047 s] Raw data (loadavg): 0.91 0.94 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 6312 0 0 0 1916 34 0 0 25 0 1 0 1844221215 17981440 4073 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 4390 4073 162 162 0 4228 0 [pid=27540] vsize: 17560 Current children cumulated CPU time (s) 19.56 Current children cumulated vsize (Kb) 19688 [startup+30.0053 s] Raw data (loadavg): 0.92 0.94 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 6312 0 0 0 2916 34 0 0 25 0 1 0 1844221215 17981440 4073 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 4390 4073 162 162 0 4228 0 [pid=27540] vsize: 17560 Current children cumulated CPU time (s) 29.56 Current children cumulated vsize (Kb) 19688 [startup+40.0069 s] Raw data (loadavg): 0.93 0.94 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 6312 0 0 0 3916 34 0 0 25 0 1 0 1844221215 17981440 4073 4294967295 134512640 135167914 3221224448 3221223204 134697042 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 4390 4073 162 162 0 4228 0 [pid=27540] vsize: 17560 Current children cumulated CPU time (s) 39.56 Current children cumulated vsize (Kb) 19688 [startup+50.0075 s] Raw data (loadavg): 0.94 0.94 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 6312 0 0 0 4916 34 0 0 25 0 1 0 1844221215 17981440 4073 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 4390 4073 162 162 0 4228 0 [pid=27540] vsize: 17560 Current children cumulated CPU time (s) 49.56 Current children cumulated vsize (Kb) 19688 [startup+60.0081 s] Raw data (loadavg): 0.95 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 6312 0 0 0 5916 35 0 0 25 0 1 0 1844221215 17981440 4073 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 4390 4073 162 162 0 4228 0 [pid=27540] vsize: 17560 Current children cumulated CPU time (s) 59.57 Current children cumulated vsize (Kb) 19688 [startup+70.0087 s] Raw data (loadavg): 0.96 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 8570 0 0 0 6898 44 0 0 25 0 1 0 1844221215 25321472 5857 4294967295 134512640 135167914 3221224448 3221207732 134697170 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 6182 5857 162 162 0 6020 0 [pid=27540] vsize: 24728 Current children cumulated CPU time (s) 69.48 Current children cumulated vsize (Kb) 26856 [startup+80.0093 s] Raw data (loadavg): 0.96 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14479 0 0 0 7850 69 0 0 25 0 1 0 1844221215 45461504 10777 4294967295 134512640 135167914 3221224448 3221209100 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 11099 10777 162 162 0 10937 0 [pid=27540] vsize: 44396 Current children cumulated CPU time (s) 79.25 Current children cumulated vsize (Kb) 46524 [startup+90.0099 s] Raw data (loadavg): 0.97 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14856 0 0 0 8845 71 0 0 25 0 1 0 1844221215 41603072 9836 4294967295 134512640 135167914 3221224448 3221220672 134844720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9836 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 89.22 Current children cumulated vsize (Kb) 42756 [startup+100.011 s] Raw data (loadavg): 0.97 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14856 0 0 0 9845 71 0 0 25 0 1 0 1844221215 41603072 9836 4294967295 134512640 135167914 3221224448 3221220320 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9836 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 99.22 Current children cumulated vsize (Kb) 42756 [startup+110.011 s] Raw data (loadavg): 0.98 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14856 0 0 0 10845 72 0 0 25 0 1 0 1844221215 41603072 9836 4294967295 134512640 135167914 3221224448 3221220928 134694338 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9836 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 109.23 Current children cumulated vsize (Kb) 42756 [startup+120.013 s] Raw data (loadavg): 0.98 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14863 0 0 0 11844 72 0 0 25 0 1 0 1844221215 41603072 9843 4294967295 134512640 135167914 3221224448 3221211280 134845893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9843 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 119.22 Current children cumulated vsize (Kb) 42756 [startup+130.013 s] Raw data (loadavg): 0.98 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14863 0 0 0 12845 72 0 0 25 0 1 0 1844221215 41603072 9843 4294967295 134512640 135167914 3221224448 3221220160 134843426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9843 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 129.23 Current children cumulated vsize (Kb) 42756 [startup+140.014 s] Raw data (loadavg): 0.98 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14863 0 0 0 13844 73 0 0 25 0 1 0 1844221215 41603072 9843 4294967295 134512640 135167914 3221224448 3221219888 134630875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9843 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 139.23 Current children cumulated vsize (Kb) 42756 [startup+150.014 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14863 0 0 0 14844 73 0 0 25 0 1 0 1844221215 41603072 9843 4294967295 134512640 135167914 3221224448 3221220560 134843420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9843 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 149.23 Current children cumulated vsize (Kb) 42756 [startup+160.014 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14863 0 0 0 15844 73 0 0 25 0 1 0 1844221215 41603072 9843 4294967295 134512640 135167914 3221224448 3221221060 134844636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9843 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 159.23 Current children cumulated vsize (Kb) 42756 [startup+170.015 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14863 0 0 0 16844 73 0 0 25 0 1 0 1844221215 41603072 9843 4294967295 134512640 135167914 3221224448 3221221024 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9843 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 169.23 Current children cumulated vsize (Kb) 42756 [startup+180.015 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14863 0 0 0 17844 73 0 0 25 0 1 0 1844221215 41603072 9843 4294967295 134512640 135167914 3221224448 3221220332 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9843 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 179.23 Current children cumulated vsize (Kb) 42756 [startup+190.017 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 14863 0 0 0 18844 73 0 0 25 0 1 0 1844221215 41603072 9843 4294967295 134512640 135167914 3221224448 3221221996 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10157 9843 162 162 0 9995 0 [pid=27540] vsize: 40628 Current children cumulated CPU time (s) 189.23 Current children cumulated vsize (Kb) 42756 [startup+200.018 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 16181 0 0 0 19841 77 0 0 25 0 1 0 1844221215 47001600 11161 4294967295 134512640 135167914 3221224448 3221208608 134844682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 11475 11161 162 162 0 11313 0 [pid=27540] vsize: 45900 Current children cumulated CPU time (s) 199.24 Current children cumulated vsize (Kb) 48028 [startup+210.018 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 16754 0 0 0 20835 80 0 0 25 0 1 0 1844221215 43950080 10416 4294967295 134512640 135167914 3221224448 3221219840 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10730 10416 162 162 0 10568 0 [pid=27540] vsize: 42920 Current children cumulated CPU time (s) 209.21 Current children cumulated vsize (Kb) 45048 [startup+220.02 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 16754 0 0 0 21835 80 0 0 25 0 1 0 1844221215 43950080 10416 4294967295 134512640 135167914 3221224448 3221220496 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10730 10416 162 162 0 10568 0 [pid=27540] vsize: 42920 Current children cumulated CPU time (s) 219.21 Current children cumulated vsize (Kb) 45048 [startup+230.02 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 16754 0 0 0 22835 80 0 0 25 0 1 0 1844221215 43950080 10416 4294967295 134512640 135167914 3221224448 3221219248 134845913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10730 10416 162 162 0 10568 0 [pid=27540] vsize: 42920 Current children cumulated CPU time (s) 229.21 Current children cumulated vsize (Kb) 45048 [startup+240.021 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 16754 0 0 0 23835 81 0 0 25 0 1 0 1844221215 43950080 10416 4294967295 134512640 135167914 3221224448 3221220384 134849148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10730 10416 162 162 0 10568 0 [pid=27540] vsize: 42920 Current children cumulated CPU time (s) 239.22 Current children cumulated vsize (Kb) 45048 [startup+250.022 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 16754 0 0 0 24835 81 0 0 25 0 1 0 1844221215 43950080 10416 4294967295 134512640 135167914 3221224448 3221221152 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10730 10416 162 162 0 10568 0 [pid=27540] vsize: 42920 Current children cumulated CPU time (s) 249.22 Current children cumulated vsize (Kb) 45048 [startup+260.022 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 16754 0 0 0 25835 81 0 0 25 0 1 0 1844221215 43950080 10416 4294967295 134512640 135167914 3221224448 3221221360 134718181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10730 10416 162 162 0 10568 0 [pid=27540] vsize: 42920 Current children cumulated CPU time (s) 259.22 Current children cumulated vsize (Kb) 45048 [startup+270.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 17414 0 0 0 26833 83 0 0 25 0 1 0 1844221215 45301760 10746 4294967295 134512640 135167914 3221224448 3221211728 134849113 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 11060 10746 162 162 0 10898 0 [pid=27540] vsize: 44240 Current children cumulated CPU time (s) 269.22 Current children cumulated vsize (Kb) 46368 [startup+280.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 19391 0 0 0 27828 88 0 0 25 0 1 0 1844221215 49348608 11734 4294967295 134512640 135167914 3221224448 3221209296 134624013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 12048 11734 162 162 0 11886 0 [pid=27540] vsize: 48192 Current children cumulated CPU time (s) 279.22 Current children cumulated vsize (Kb) 50320 [startup+290.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 24531 0 0 0 28791 109 0 0 25 0 1 0 1844221215 43950080 10416 4294967295 134512640 135167914 3221224448 3221209744 134624410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 10730 10416 162 162 0 10568 0 [pid=27540] vsize: 42920 Current children cumulated CPU time (s) 289.06 Current children cumulated vsize (Kb) 45048 [startup+300.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 26838 0 0 0 29784 116 0 0 25 0 1 0 1844221215 49348608 11734 4294967295 134512640 135167914 3221224448 3221209248 134722591 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 12048 11734 162 162 0 11886 0 [pid=27540] vsize: 48192 Current children cumulated CPU time (s) 299.06 Current children cumulated vsize (Kb) 50320 [startup+310.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 32327 0 0 0 30747 136 0 0 25 0 1 0 1844221215 66433024 15905 4294967295 134512640 135167914 3221224448 3221223232 134623605 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 16219 15905 162 162 0 16057 0 [pid=27540] vsize: 64876 Current children cumulated CPU time (s) 308.89 Current children cumulated vsize (Kb) 67004 [startup+320.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 32327 0 0 0 31746 137 0 0 25 0 1 0 1844221215 55631872 13268 4294967295 134512640 135167914 3221224448 3221209440 134844731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 13582 13268 162 162 0 13420 0 [pid=27540] vsize: 54328 Current children cumulated CPU time (s) 318.89 Current children cumulated vsize (Kb) 56456 [startup+330.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 32327 0 0 0 32746 137 0 0 25 0 1 0 1844221215 55631872 13268 4294967295 134512640 135167914 3221224448 3221208544 134845737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 13582 13268 162 162 0 13420 0 [pid=27540] vsize: 54328 Current children cumulated CPU time (s) 328.89 Current children cumulated vsize (Kb) 56456 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 37172 0 0 0 33714 155 0 0 25 0 1 0 1844221215 75476992 18113 4294967295 134512640 135167914 3221224448 3221208736 134844653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18427 18113 162 162 0 18265 0 [pid=27540] vsize: 73708 Current children cumulated CPU time (s) 338.75 Current children cumulated vsize (Kb) 75836 [startup+350.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 34683 168 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221208020 134695540 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 348.57 Current children cumulated vsize (Kb) 75680 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 35682 169 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221209888 134844736 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 358.57 Current children cumulated vsize (Kb) 75680 [startup+370.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 36682 169 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221223232 134623590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 368.57 Current children cumulated vsize (Kb) 75680 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 37682 169 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221219696 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 378.57 Current children cumulated vsize (Kb) 75680 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 38682 169 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221220220 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 388.57 Current children cumulated vsize (Kb) 75680 [startup+400.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 39682 169 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221220332 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 398.57 Current children cumulated vsize (Kb) 75680 [startup+410.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 40682 169 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221220864 134843113 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 408.57 Current children cumulated vsize (Kb) 75680 [startup+420.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 41682 170 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221220784 134844715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 418.58 Current children cumulated vsize (Kb) 75680 [startup+430.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 42682 170 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221220960 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 428.58 Current children cumulated vsize (Kb) 75680 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 43682 170 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221220240 134629231 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 438.58 Current children cumulated vsize (Kb) 75680 [startup+450.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 44681 171 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221221120 134630746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 448.58 Current children cumulated vsize (Kb) 75680 [startup+460.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 45681 171 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221221440 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 458.58 Current children cumulated vsize (Kb) 75680 [startup+470.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 46681 171 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221215404 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 468.58 Current children cumulated vsize (Kb) 75680 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 47679 173 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221209088 134696034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 478.58 Current children cumulated vsize (Kb) 75680 [startup+490.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 48678 174 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221208896 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 488.58 Current children cumulated vsize (Kb) 75680 [startup+500.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 49679 174 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221210016 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 498.59 Current children cumulated vsize (Kb) 75680 [startup+510.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 50679 174 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221212236 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 508.59 Current children cumulated vsize (Kb) 75680 [startup+520.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 51679 174 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221212956 134694368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 518.59 Current children cumulated vsize (Kb) 75680 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 52679 174 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221211184 134619137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 528.59 Current children cumulated vsize (Kb) 75680 [startup+540.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39770 0 0 0 53680 174 0 0 25 0 1 0 1844221215 75317248 18074 4294967295 134512640 135167914 3221224448 3221221236 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18388 18074 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 538.6 Current children cumulated vsize (Kb) 75680 [startup+550.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39782 0 0 0 54680 174 0 0 25 0 1 0 1844221215 75317248 18086 4294967295 134512640 135167914 3221224448 3221211984 134623813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18388 18086 162 162 0 18226 0 [pid=27540] vsize: 73552 Current children cumulated CPU time (s) 548.6 Current children cumulated vsize (Kb) 75680 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39786 0 0 0 55680 174 0 0 25 0 1 0 1844221215 75333632 18090 4294967295 134512640 135167914 3221224448 3221221024 134844694 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18392 18090 162 162 0 18230 0 [pid=27540] vsize: 73568 Current children cumulated CPU time (s) 558.6 Current children cumulated vsize (Kb) 75696 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39786 0 0 0 56680 174 0 0 25 0 1 0 1844221215 75333632 18090 4294967295 134512640 135167914 3221224448 3221220224 134843030 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18392 18090 162 162 0 18230 0 [pid=27540] vsize: 73568 Current children cumulated CPU time (s) 568.6 Current children cumulated vsize (Kb) 75696 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39786 0 0 0 57681 174 0 0 25 0 1 0 1844221215 75333632 18090 4294967295 134512640 135167914 3221224448 3221220912 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18392 18090 162 162 0 18230 0 [pid=27540] vsize: 73568 Current children cumulated CPU time (s) 578.61 Current children cumulated vsize (Kb) 75696 [startup+590.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39786 0 0 0 58681 174 0 0 25 0 1 0 1844221215 75333632 18090 4294967295 134512640 135167914 3221224448 3221221616 134849108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18392 18090 162 162 0 18230 0 [pid=27540] vsize: 73568 Current children cumulated CPU time (s) 588.61 Current children cumulated vsize (Kb) 75696 [startup+600.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39786 0 0 0 59681 174 0 0 25 0 1 0 1844221215 75333632 18090 4294967295 134512640 135167914 3221224448 3221214960 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18392 18090 162 162 0 18230 0 [pid=27540] vsize: 73568 Current children cumulated CPU time (s) 598.61 Current children cumulated vsize (Kb) 75696 [startup+610.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39786 0 0 0 60681 174 0 0 25 0 1 0 1844221215 75333632 18090 4294967295 134512640 135167914 3221224448 3221220384 134694489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18392 18090 162 162 0 18230 0 [pid=27540] vsize: 73568 Current children cumulated CPU time (s) 608.61 Current children cumulated vsize (Kb) 75696 [startup+620.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39786 0 0 0 61681 174 0 0 25 0 1 0 1844221215 75333632 18090 4294967295 134512640 135167914 3221224448 3221221264 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27540/statm): 18392 18090 162 162 0 18230 0 [pid=27540] vsize: 73568 Current children cumulated CPU time (s) 618.61 Current children cumulated vsize (Kb) 75696 [startup+630.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39786 0 0 0 62681 175 0 0 25 0 1 0 1844221215 75333632 18090 4294967295 134512640 135167914 3221224448 3221219644 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18392 18090 162 162 0 18230 0 [pid=27540] vsize: 73568 Current children cumulated CPU time (s) 628.62 Current children cumulated vsize (Kb) 75696 [startup+640.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 63681 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3220903648 134843404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 638.62 Current children cumulated vsize (Kb) 75976 [startup+650.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 64681 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3220913568 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 648.62 Current children cumulated vsize (Kb) 75976 [startup+660.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 65682 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3220912132 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 658.63 Current children cumulated vsize (Kb) 75976 [startup+670.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 66682 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221218928 134723225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 668.63 Current children cumulated vsize (Kb) 75976 [startup+680.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 67682 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221218928 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 678.63 Current children cumulated vsize (Kb) 75976 [startup+690.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 68682 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221219700 134849060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 688.63 Current children cumulated vsize (Kb) 75976 [startup+700.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 69682 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221219680 134843404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 698.63 Current children cumulated vsize (Kb) 75976 [startup+710.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 70682 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220080 134844725 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 708.63 Current children cumulated vsize (Kb) 75976 [startup+720.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 71683 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220320 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 718.64 Current children cumulated vsize (Kb) 75976 [startup+730.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 72683 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221219824 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 728.64 Current children cumulated vsize (Kb) 75976 [startup+740.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 73683 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221219500 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 738.64 Current children cumulated vsize (Kb) 75976 [startup+750.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 74683 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220000 134522502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 748.64 Current children cumulated vsize (Kb) 75976 [startup+760.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 75683 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220388 134849060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 758.64 Current children cumulated vsize (Kb) 75976 [startup+770.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 76684 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221219980 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 768.65 Current children cumulated vsize (Kb) 75976 [startup+780.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 77684 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220364 134845882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 778.65 Current children cumulated vsize (Kb) 75976 [startup+790.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 78684 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220496 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 788.65 Current children cumulated vsize (Kb) 75976 [startup+800.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 79684 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220048 134849179 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 798.65 Current children cumulated vsize (Kb) 75976 [startup+810.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 80684 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220364 134844675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 808.65 Current children cumulated vsize (Kb) 75976 [startup+820.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 81684 175 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220384 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 818.65 Current children cumulated vsize (Kb) 75976 [startup+830.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 82685 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220028 134722208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 828.67 Current children cumulated vsize (Kb) 75976 [startup+840.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 83685 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220560 134843074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 838.67 Current children cumulated vsize (Kb) 75976 [startup+850.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 84685 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220044 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 848.67 Current children cumulated vsize (Kb) 75976 [startup+860.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 85685 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220576 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 858.67 Current children cumulated vsize (Kb) 75976 [startup+870.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 86685 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220060 134522184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 868.67 Current children cumulated vsize (Kb) 75976 [startup+880.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 87685 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220364 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 878.67 Current children cumulated vsize (Kb) 75976 [startup+890.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 88686 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220136 134718177 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 888.68 Current children cumulated vsize (Kb) 75976 [startup+900.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 89686 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220368 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 898.68 Current children cumulated vsize (Kb) 75976 [startup+910.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 90686 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220388 134849147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 908.68 Current children cumulated vsize (Kb) 75976 [startup+920.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 91686 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220208 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 918.68 Current children cumulated vsize (Kb) 75976 [startup+930.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 92687 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220672 134696738 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 928.69 Current children cumulated vsize (Kb) 75976 [startup+940.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 93687 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220672 134843139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 938.69 Current children cumulated vsize (Kb) 75976 [startup+950.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 94687 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220556 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 948.69 Current children cumulated vsize (Kb) 75976 [startup+960.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 95687 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220576 134849071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 958.69 Current children cumulated vsize (Kb) 75976 [startup+970.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 96687 176 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220412 134522184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 968.69 Current children cumulated vsize (Kb) 75976 [startup+980.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 97687 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220784 134844723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 978.7 Current children cumulated vsize (Kb) 75976 [startup+990.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 98687 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220208 134694504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 988.7 Current children cumulated vsize (Kb) 75976 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 99687 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220496 134843402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 998.7 Current children cumulated vsize (Kb) 75976 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 100687 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221088 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1008.7 Current children cumulated vsize (Kb) 75976 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 101688 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220832 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1018.71 Current children cumulated vsize (Kb) 75976 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 102688 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221040 134843074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1028.71 Current children cumulated vsize (Kb) 75976 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 103688 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220544 134522839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1038.71 Current children cumulated vsize (Kb) 75976 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 104688 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221292 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1048.71 Current children cumulated vsize (Kb) 75976 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 105688 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220844 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1058.71 Current children cumulated vsize (Kb) 75976 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 106688 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220592 134628668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1068.71 Current children cumulated vsize (Kb) 75976 [startup+1080.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 107689 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1078.72 Current children cumulated vsize (Kb) 75976 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 108689 177 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221760 134722539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1088.72 Current children cumulated vsize (Kb) 75976 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 109689 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220936 134849057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1098.73 Current children cumulated vsize (Kb) 75976 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 110689 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221328 134844718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1108.73 Current children cumulated vsize (Kb) 75976 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 111689 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221280 134693561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1118.73 Current children cumulated vsize (Kb) 75976 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 112689 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220892 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1128.73 Current children cumulated vsize (Kb) 75976 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 113690 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220772 134629284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1138.74 Current children cumulated vsize (Kb) 75976 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 114690 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220608 134844682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1148.74 Current children cumulated vsize (Kb) 75976 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 115690 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1158.74 Current children cumulated vsize (Kb) 75976 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 116690 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220920 134722513 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1168.74 Current children cumulated vsize (Kb) 75976 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 117690 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220540 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1178.74 Current children cumulated vsize (Kb) 75976 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 118690 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220848 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1188.74 Current children cumulated vsize (Kb) 75976 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 119691 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221220880 134722532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1198.75 Current children cumulated vsize (Kb) 75976 [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 120691 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221276 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1208.75 Current children cumulated vsize (Kb) 75976 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27540 Raw data (/proc/27535/stat): 27535 (minisat+_script) S 27534 27535 19316 0 -1 0 314 478 0 0 0 1 4 1 19 0 1 0 1844221203 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27535/statm): 532 234 485 147 0 385 0 [pid=27535] vsize: 2128 Raw data (/proc/27540/stat): 27540 (minisat+_bignum) R 27535 27535 19316 0 -1 0 39856 0 0 0 120691 178 0 0 25 0 1 0 1844221215 75620352 18160 4294967295 134512640 135167914 3221224448 3221221200 134843402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27540/statm): 18462 18160 162 162 0 18300 0 [pid=27540] vsize: 73848 Current children cumulated CPU time (s) 1208.75 Current children cumulated vsize (Kb) 75976 Sending SIGTERM to -27535 Sleeping 2 seconds One traced child (pid=27535) ended because it received signal 15 (SIGTERM) One traced child (pid=27540) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.11 CPU time (s): 1208.74 CPU user time (s): 1206.92 CPU system time (s): 1.81972 CPU usage (%): 99.8861 Max. virtual memory (cumulated for all children) (Kb): 75976
ERROR: no interpretation found !