Name | mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core4872-1529.opb |
MD5SUM | 7eea141e02c7a2753145fd63f1e9087d |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 253696000000000 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 24865 |
Biggest coefficient in the objective function | 52428800000000000 |
Number of bits for the biggest coefficient in the objective function | 56 |
Sum of the numbers in the objective function | 226690477012582900 |
Number of bits of the sum of numbers in the objective function | 58 |
Biggest number in a constraint | 1280000000000000000000 |
Number of bits of the biggest number in a constraint | 71 |
Biggest sum of numbers in a constraint | 1280226690477012549632 |
Number of bits of the biggest sum of numbers | 71 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1206.48 |
Number of variables | 24865 |
Total number of constraints | 29520 |
Number of constraints which are clauses | 4872 |
Number of constraints which are cardinality constraints (but not clauses) | 24647 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 24865 |
LAUNCH ON wulflinc13 THE 2005-09-20 05:34:55 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3487 boxname=wulflinc13 idbench=1143 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 7eea141e02c7a2753145fd63f1e9087d /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-core4872-1529.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-core4872-1529.opb IDLAUNCH: 3487 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 888236 kB Buffers: 32976 kB Cached: 85732 kB SwapCached: 700 kB Active: 47940 kB Inactive: 73428 kB HighTotal: 131008 kB HighFree: 41384 kB LowTotal: 903652 kB LowFree: 846852 kB SwapTotal: 2097136 kB SwapFree: 2095936 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5744 kB Slab: 19380 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 05:55:06 (client local time) WITH STATUS 0 IN 1208.74 SECONDS stats: 3487 7 1208.74 0
c Parsing PB file... c PARSE ERROR! [line 24660] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 4760 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: =================================== c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 325]---> Adder-cost: 35658 maxlim: 8607 bits: 15/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 254172 1062419 | 84724 0 0 nan | 0.000 % | c | 100 | 254172 1062419 | 93196 100 307 3.1 | 0.091 % | c | 250 | 254172 1062419 | 102516 250 778 3.1 | 0.091 % | c | 475 | 254172 1062419 | 112767 475 1456 3.1 | 0.091 % | c | 812 | 254172 1062419 | 124044 812 2487 3.1 | 0.091 % | c | 1318 | 254172 1062419 | 136448 1318 4056 3.1 | 0.091 % | c | 2077 | 254172 1062419 | 150093 2077 6476 3.1 | 0.091 % | c | 3216 | 254172 1062419 | 165103 3216 9993 3.1 | 0.091 % | c | 4924 | 254172 1062419 | 181613 4924 15694 3.2 | 0.091 % | c | 7487 | 254172 1062419 | 199774 7487 24396 3.3 | 0.091 % | c | 11333 | 254172 1062419 | 219752 11333 37608 3.3 | 0.091 % | c | 17099 | 254172 1062419 | 241727 17099 59148 3.5 | 0.091 % | c | 25748 | 254172 1062419 | 265900 25748 92223 3.6 | 0.091 % | c | 38722 | 254172 1062419 | 292490 38722 148384 3.8 | 0.091 % | c | 58183 | 254172 1062419 | 321739 58183 255683 4.4 | 0.091 % |
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/22739/stat): 22739 (minisat+_script) R 22738 22739 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797849082 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/22739/statm): 174 3 169 147 0 27 0 [pid=22739] 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=22740 New process pid=22741 New process pid=22742 execve syscall for /bin/sed executable One traced child (pid=22741) 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=22742) exited with status: 0 One traced child (pid=22740) exited with status: 0 New process pid=22743 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-core4872-1529.opb One traced child (pid=22743) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=22744 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-core4872-1529.opb [startup+10.0041 s] Raw data (loadavg): 0.93 0.95 0.90 1/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) T 22739 22739 1333 0 -1 0 3444 0 4 0 904 25 0 0 25 0 1 0 1797849119 14757888 3392 4294967295 134512640 135167914 3221224432 3221223272 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22744/statm): 3603 3392 162 162 0 3441 0 [pid=22744] vsize: 14412 Current children cumulated CPU time (s) 9.57 Current children cumulated vsize (Kb) 16540 [startup+20.0048 s] Raw data (loadavg): 0.94 0.95 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 8955 0 4 0 1857 50 0 0 25 0 1 0 1797849119 27009024 6385 4294967295 134512640 135167914 3221224432 3217706560 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6594 6385 162 162 0 6432 0 [pid=22744] vsize: 26376 Current children cumulated CPU time (s) 19.35 Current children cumulated vsize (Kb) 28504 [startup+30.0054 s] Raw data (loadavg): 0.95 0.95 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 8996 0 4 0 2857 50 0 0 25 0 1 0 1797849119 27201536 6426 4294967295 134512640 135167914 3221224432 3218156540 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6641 6426 162 162 0 6479 0 [pid=22744] vsize: 26564 Current children cumulated CPU time (s) 29.35 Current children cumulated vsize (Kb) 28692 [startup+40.0061 s] Raw data (loadavg): 0.95 0.95 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9041 0 4 0 3857 50 0 0 25 0 1 0 1797849119 27373568 6471 4294967295 134512640 135167914 3221224432 3218447856 134844676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6683 6471 162 162 0 6521 0 [pid=22744] vsize: 26732 Current children cumulated CPU time (s) 39.35 Current children cumulated vsize (Kb) 28860 [startup+50.0067 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9044 0 4 0 4857 50 0 0 25 0 1 0 1797849119 27373568 6474 4294967295 134512640 135167914 3221224432 3218677388 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6683 6474 162 162 0 6521 0 [pid=22744] vsize: 26732 Current children cumulated CPU time (s) 49.35 Current children cumulated vsize (Kb) 28860 [startup+60.0074 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9047 0 4 0 5858 50 0 0 25 0 1 0 1797849119 27373568 6477 4294967295 134512640 135167914 3221224432 3218872012 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6683 6477 162 162 0 6521 0 [pid=22744] vsize: 26732 Current children cumulated CPU time (s) 59.36 Current children cumulated vsize (Kb) 28860 [startup+70.008 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9051 0 4 0 6858 50 0 0 25 0 1 0 1797849119 27385856 6481 4294967295 134512640 135167914 3221224432 3219043852 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6686 6481 162 162 0 6524 0 [pid=22744] vsize: 26744 Current children cumulated CPU time (s) 69.36 Current children cumulated vsize (Kb) 28872 [startup+80.0087 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 7858 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3218732716 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0 [pid=22744] vsize: 26940 Current children cumulated CPU time (s) 79.36 Current children cumulated vsize (Kb) 29068 [startup+90.0094 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 8858 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3218344656 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0 [pid=22744] vsize: 26940 Current children cumulated CPU time (s) 89.36 Current children cumulated vsize (Kb) 29068 [startup+100.01 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 9858 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3218179852 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0 [pid=22744] vsize: 26940 Current children cumulated CPU time (s) 99.36 Current children cumulated vsize (Kb) 29068 [startup+110.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 10859 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3217994860 134693585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0 [pid=22744] vsize: 26940 Current children cumulated CPU time (s) 109.37 Current children cumulated vsize (Kb) 29068 [startup+120.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 11859 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3217754952 134693553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0 [pid=22744] vsize: 26940 Current children cumulated CPU time (s) 119.37 Current children cumulated vsize (Kb) 29068 [startup+130.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 12859 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3217449836 134722229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0 [pid=22744] vsize: 26940 Current children cumulated CPU time (s) 129.37 Current children cumulated vsize (Kb) 29068 [startup+140.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9231 0 4 0 13858 51 0 0 25 0 1 0 1797849119 28184576 6661 4294967295 134512640 135167914 3221224432 3217771532 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6881 6661 162 162 0 6719 0 [pid=22744] vsize: 27524 Current children cumulated CPU time (s) 139.37 Current children cumulated vsize (Kb) 29652 [startup+150.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9244 0 4 0 14858 51 0 0 25 0 1 0 1797849119 28188672 6674 4294967295 134512640 135167914 3221224432 3218700896 134693566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6882 6674 162 162 0 6720 0 [pid=22744] vsize: 27528 Current children cumulated CPU time (s) 149.37 Current children cumulated vsize (Kb) 29656 [startup+160.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9268 0 4 0 15859 51 0 0 25 0 1 0 1797849119 28459008 6698 4294967295 134512640 135167914 3221224432 3218611152 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6948 6698 162 162 0 6786 0 [pid=22744] vsize: 27792 Current children cumulated CPU time (s) 159.38 Current children cumulated vsize (Kb) 29920 [startup+170.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9268 0 4 0 16859 51 0 0 25 0 1 0 1797849119 28459008 6698 4294967295 134512640 135167914 3221224432 3217686752 134845890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 6948 6698 162 162 0 6786 0 [pid=22744] vsize: 27792 Current children cumulated CPU time (s) 169.38 Current children cumulated vsize (Kb) 29920 [startup+180.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9363 0 4 0 17858 51 0 0 25 0 1 0 1797849119 28819456 6793 4294967295 134512640 135167914 3221224432 3217755600 134843160 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7036 6793 162 162 0 6874 0 [pid=22744] vsize: 28144 Current children cumulated CPU time (s) 179.37 Current children cumulated vsize (Kb) 30272 [startup+190.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9578 0 4 0 18858 52 0 0 25 0 1 0 1797849119 29306880 6924 4294967295 134512640 135167914 3221224432 3218674220 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7155 6924 162 162 0 6993 0 [pid=22744] vsize: 28620 Current children cumulated CPU time (s) 189.38 Current children cumulated vsize (Kb) 30748 [startup+200.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9603 0 4 0 19858 52 0 0 25 0 1 0 1797849119 29384704 6949 4294967295 134512640 135167914 3221224432 3219026336 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7174 6949 162 162 0 7012 0 [pid=22744] vsize: 28696 Current children cumulated CPU time (s) 199.38 Current children cumulated vsize (Kb) 30824 [startup+210.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9603 0 4 0 20858 52 0 0 25 0 1 0 1797849119 29384704 6949 4294967295 134512640 135167914 3221224432 3218173120 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7174 6949 162 162 0 7012 0 [pid=22744] vsize: 28696 Current children cumulated CPU time (s) 209.38 Current children cumulated vsize (Kb) 30824 [startup+220.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9603 0 4 0 21858 52 0 0 25 0 1 0 1797849119 29384704 6949 4294967295 134512640 135167914 3221224432 3217769292 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7174 6949 162 162 0 7012 0 [pid=22744] vsize: 28696 Current children cumulated CPU time (s) 219.38 Current children cumulated vsize (Kb) 30824 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9653 0 4 0 22858 53 0 0 25 0 1 0 1797849119 29589504 6999 4294967295 134512640 135167914 3221224432 3217310512 134694419 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7224 6999 162 162 0 7062 0 [pid=22744] vsize: 28896 Current children cumulated CPU time (s) 229.39 Current children cumulated vsize (Kb) 31024 [startup+240.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9725 0 4 0 23856 53 0 0 25 0 1 0 1797849119 29827072 7071 4294967295 134512640 135167914 3221224432 3218258416 134844715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7282 7071 162 162 0 7120 0 [pid=22744] vsize: 29128 Current children cumulated CPU time (s) 239.37 Current children cumulated vsize (Kb) 31256 [startup+250.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9763 0 4 0 24856 53 0 0 25 0 1 0 1797849119 30339072 7109 4294967295 134512640 135167914 3221224432 3218984400 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7407 7109 162 162 0 7245 0 [pid=22744] vsize: 29628 Current children cumulated CPU time (s) 249.37 Current children cumulated vsize (Kb) 31756 [startup+260.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9772 0 4 0 25856 53 0 0 25 0 1 0 1797849119 30367744 7118 4294967295 134512640 135167914 3221224432 3217582608 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7414 7118 162 162 0 7252 0 [pid=22744] vsize: 29656 Current children cumulated CPU time (s) 259.37 Current children cumulated vsize (Kb) 31784 [startup+270.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9896 0 4 0 26855 54 0 0 25 0 1 0 1797849119 30818304 7242 4294967295 134512640 135167914 3221224432 3218307312 134694419 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7524 7242 162 162 0 7362 0 [pid=22744] vsize: 30096 Current children cumulated CPU time (s) 269.37 Current children cumulated vsize (Kb) 32224 [startup+280.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10261 0 4 0 27854 55 0 0 25 0 1 0 1797849119 31936512 7524 4294967295 134512640 135167914 3221224432 3218944160 134524005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7797 7524 162 162 0 7635 0 [pid=22744] vsize: 31188 Current children cumulated CPU time (s) 279.37 Current children cumulated vsize (Kb) 33316 [startup+290.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10272 0 4 0 28854 55 0 0 25 0 1 0 1797849119 31629312 7452 4294967295 134512640 135167914 3221224432 3218831244 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7722 7452 162 162 0 7560 0 [pid=22744] vsize: 30888 Current children cumulated CPU time (s) 289.37 Current children cumulated vsize (Kb) 33016 [startup+300.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10272 0 4 0 29854 55 0 0 25 0 1 0 1797849119 31629312 7452 4294967295 134512640 135167914 3221224432 3218484880 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7722 7452 162 162 0 7560 0 [pid=22744] vsize: 30888 Current children cumulated CPU time (s) 299.37 Current children cumulated vsize (Kb) 33016 [startup+310.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10272 0 4 0 30855 55 0 0 25 0 1 0 1797849119 31629312 7452 4294967295 134512640 135167914 3221224432 3218067504 134844723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7722 7452 162 162 0 7560 0 [pid=22744] vsize: 30888 Current children cumulated CPU time (s) 309.38 Current children cumulated vsize (Kb) 33016 [startup+320.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10282 0 4 0 31855 55 0 0 25 0 1 0 1797849119 31670272 7462 4294967295 134512640 135167914 3221224432 3217502172 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7732 7462 162 162 0 7570 0 [pid=22744] vsize: 30928 Current children cumulated CPU time (s) 319.38 Current children cumulated vsize (Kb) 33056 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10373 0 4 0 32854 55 0 0 25 0 1 0 1797849119 32010240 7553 4294967295 134512640 135167914 3221224432 3217884320 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7815 7553 162 162 0 7653 0 [pid=22744] vsize: 31260 Current children cumulated CPU time (s) 329.37 Current children cumulated vsize (Kb) 33388 [startup+340.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10412 0 4 0 33854 55 0 0 25 0 1 0 1797849119 32129024 7592 4294967295 134512640 135167914 3221224432 3218628224 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7844 7592 162 162 0 7682 0 [pid=22744] vsize: 31376 Current children cumulated CPU time (s) 339.37 Current children cumulated vsize (Kb) 33504 [startup+350.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10441 0 4 0 34854 55 0 0 25 0 1 0 1797849119 32219136 7621 4294967295 134512640 135167914 3221224432 3218949888 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7866 7621 162 162 0 7704 0 [pid=22744] vsize: 31464 Current children cumulated CPU time (s) 349.37 Current children cumulated vsize (Kb) 33592 [startup+360.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10441 0 4 0 35854 55 0 0 25 0 1 0 1797849119 32219136 7621 4294967295 134512640 135167914 3221224432 3217823920 134694439 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7866 7621 162 162 0 7704 0 [pid=22744] vsize: 31464 Current children cumulated CPU time (s) 359.37 Current children cumulated vsize (Kb) 33592 [startup+370.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10526 0 4 0 36853 56 0 0 25 0 1 0 1797849119 32550912 7706 4294967295 134512640 135167914 3221224432 3217585608 134694369 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7947 7706 162 162 0 7785 0 [pid=22744] vsize: 31788 Current children cumulated CPU time (s) 369.37 Current children cumulated vsize (Kb) 33916 [startup+380.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10578 0 4 0 37852 56 0 0 25 0 1 0 1797849119 32710656 7758 4294967295 134512640 135167914 3221224432 3218555072 134849196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 7986 7758 162 162 0 7824 0 [pid=22744] vsize: 31944 Current children cumulated CPU time (s) 379.36 Current children cumulated vsize (Kb) 34072 [startup+390.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10639 0 4 0 38852 57 0 0 25 0 1 0 1797849119 32919552 7654 4294967295 134512640 135167914 3221224432 3221222384 134523161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 8037 7654 162 162 0 7875 0 [pid=22744] vsize: 32148 Current children cumulated CPU time (s) 389.37 Current children cumulated vsize (Kb) 34276 [startup+400.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36239 0 4 0 39720 139 0 0 25 0 1 0 1797849119 119693312 28376 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22744/statm): 29222 28376 162 162 0 29060 0 [pid=22744] vsize: 116888 Current children cumulated CPU time (s) 398.87 Current children cumulated vsize (Kb) 119016 [startup+410.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36290 0 4 0 40718 140 0 0 25 0 1 0 1797849119 119910400 28427 4294967295 134512640 135167914 3221224432 3221223104 134567641 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29275 28427 162 162 0 29113 0 [pid=22744] vsize: 117100 Current children cumulated CPU time (s) 408.86 Current children cumulated vsize (Kb) 119228 [startup+420.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36300 0 4 0 41719 140 0 0 25 0 1 0 1797849119 119947264 28437 4294967295 134512640 135167914 3221224432 3221223136 134562877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29284 28437 162 162 0 29122 0 [pid=22744] vsize: 117136 Current children cumulated CPU time (s) 418.87 Current children cumulated vsize (Kb) 119264 [startup+430.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36312 0 4 0 42719 140 0 0 25 0 1 0 1797849119 119988224 28449 4294967295 134512640 135167914 3221224432 3221223232 134563952 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29294 28449 162 162 0 29132 0 [pid=22744] vsize: 117176 Current children cumulated CPU time (s) 428.87 Current children cumulated vsize (Kb) 119304 [startup+440.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36332 0 4 0 43719 140 0 0 25 0 1 0 1797849119 120094720 28469 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29320 28469 162 162 0 29158 0 [pid=22744] vsize: 117280 Current children cumulated CPU time (s) 438.87 Current children cumulated vsize (Kb) 119408 [startup+450.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36338 0 4 0 44719 140 0 0 25 0 1 0 1797849119 120102912 28475 4294967295 134512640 135167914 3221224432 3221223092 134567725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29322 28475 162 162 0 29160 0 [pid=22744] vsize: 117288 Current children cumulated CPU time (s) 448.87 Current children cumulated vsize (Kb) 119416 [startup+460.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36349 0 4 0 45719 140 0 0 25 0 1 0 1797849119 120139776 28486 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29331 28486 162 162 0 29169 0 [pid=22744] vsize: 117324 Current children cumulated CPU time (s) 458.87 Current children cumulated vsize (Kb) 119452 [startup+470.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36358 0 4 0 46719 140 0 0 25 0 1 0 1797849119 120172544 28495 4294967295 134512640 135167914 3221224432 3221223136 134566390 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29339 28495 162 162 0 29177 0 [pid=22744] vsize: 117356 Current children cumulated CPU time (s) 468.87 Current children cumulated vsize (Kb) 119484 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36370 0 4 0 47719 140 0 0 25 0 1 0 1797849119 120213504 28507 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29349 28507 162 162 0 29187 0 [pid=22744] vsize: 117396 Current children cumulated CPU time (s) 478.87 Current children cumulated vsize (Kb) 119524 [startup+490.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36379 0 4 0 48719 140 0 0 25 0 1 0 1797849119 120246272 28516 4294967295 134512640 135167914 3221224432 3221223092 134567739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22744/statm): 29357 28516 162 162 0 29195 0 [pid=22744] vsize: 117428 Current children cumulated CPU time (s) 488.87 Current children cumulated vsize (Kb) 119556 [startup+500.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36389 0 4 0 49718 141 0 0 25 0 1 0 1797849119 120283136 28526 4294967295 134512640 135167914 3221224432 3221223092 134567745 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29366 28526 162 162 0 29204 0 [pid=22744] vsize: 117464 Current children cumulated CPU time (s) 498.87 Current children cumulated vsize (Kb) 119592 [startup+510.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36416 0 4 0 50718 141 0 0 25 0 1 0 1797849119 120451072 28553 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29407 28553 162 162 0 29245 0 [pid=22744] vsize: 117628 Current children cumulated CPU time (s) 508.87 Current children cumulated vsize (Kb) 119756 [startup+520.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36417 0 4 0 51719 141 0 0 25 0 1 0 1797849119 120451072 28554 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29407 28554 162 162 0 29245 0 [pid=22744] vsize: 117628 Current children cumulated CPU time (s) 518.88 Current children cumulated vsize (Kb) 119756 [startup+530.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36418 0 4 0 52719 141 0 0 25 0 1 0 1797849119 120451072 28555 4294967295 134512640 135167914 3221224432 3221223092 134567725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29407 28555 162 162 0 29245 0 [pid=22744] vsize: 117628 Current children cumulated CPU time (s) 528.88 Current children cumulated vsize (Kb) 119756 [startup+540.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36425 0 4 0 53719 141 0 0 25 0 1 0 1797849119 120475648 28562 4294967295 134512640 135167914 3221224432 3221223092 134567777 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29413 28562 162 162 0 29251 0 [pid=22744] vsize: 117652 Current children cumulated CPU time (s) 538.88 Current children cumulated vsize (Kb) 119780 [startup+550.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36434 0 4 0 54719 141 0 0 25 0 1 0 1797849119 120508416 28571 4294967295 134512640 135167914 3221224432 3221223204 134558992 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29421 28571 162 162 0 29259 0 [pid=22744] vsize: 117684 Current children cumulated CPU time (s) 548.88 Current children cumulated vsize (Kb) 119812 [startup+560.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36443 0 4 0 55719 141 0 0 25 0 1 0 1797849119 120541184 28580 4294967295 134512640 135167914 3221224432 3221223168 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29429 28580 162 162 0 29267 0 [pid=22744] vsize: 117716 Current children cumulated CPU time (s) 558.88 Current children cumulated vsize (Kb) 119844 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36451 0 4 0 56719 141 0 0 25 0 1 0 1797849119 120569856 28588 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29436 28588 162 162 0 29274 0 [pid=22744] vsize: 117744 Current children cumulated CPU time (s) 568.88 Current children cumulated vsize (Kb) 119872 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36461 0 4 0 57719 142 0 0 25 0 1 0 1797849119 120606720 28598 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29445 28598 162 162 0 29283 0 [pid=22744] vsize: 117780 Current children cumulated CPU time (s) 578.89 Current children cumulated vsize (Kb) 119908 [startup+590.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36469 0 4 0 58719 142 0 0 25 0 1 0 1797849119 120635392 28606 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29452 28606 162 162 0 29290 0 [pid=22744] vsize: 117808 Current children cumulated CPU time (s) 588.89 Current children cumulated vsize (Kb) 119936 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36478 0 4 0 59719 142 0 0 25 0 1 0 1797849119 120668160 28615 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29460 28615 162 162 0 29298 0 [pid=22744] vsize: 117840 Current children cumulated CPU time (s) 598.89 Current children cumulated vsize (Kb) 119968 [startup+610.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36489 0 4 0 60718 142 0 0 25 0 1 0 1797849119 120709120 28626 4294967295 134512640 135167914 3221224432 3221223184 134559182 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29470 28626 162 162 0 29308 0 [pid=22744] vsize: 117880 Current children cumulated CPU time (s) 608.88 Current children cumulated vsize (Kb) 120008 [startup+620.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36500 0 4 0 61718 142 0 0 25 0 1 0 1797849119 120750080 28637 4294967295 134512640 135167914 3221224432 3221223092 134567793 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29480 28637 162 162 0 29318 0 [pid=22744] vsize: 117920 Current children cumulated CPU time (s) 618.88 Current children cumulated vsize (Kb) 120048 [startup+630.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36516 0 4 0 62718 142 0 0 25 0 1 0 1797849119 120811520 28653 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29495 28653 162 162 0 29333 0 [pid=22744] vsize: 117980 Current children cumulated CPU time (s) 628.88 Current children cumulated vsize (Kb) 120108 [startup+640.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36527 0 4 0 63718 142 0 0 25 0 1 0 1797849119 120852480 28664 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29505 28664 162 162 0 29343 0 [pid=22744] vsize: 118020 Current children cumulated CPU time (s) 638.88 Current children cumulated vsize (Kb) 120148 [startup+650.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36536 0 4 0 64719 142 0 0 25 0 1 0 1797849119 120885248 28673 4294967295 134512640 135167914 3221224432 3221223136 134562869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29513 28673 162 162 0 29351 0 [pid=22744] vsize: 118052 Current children cumulated CPU time (s) 648.89 Current children cumulated vsize (Kb) 120180 [startup+660.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36544 0 4 0 65719 142 0 0 25 0 1 0 1797849119 120913920 28681 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29520 28681 162 162 0 29358 0 [pid=22744] vsize: 118080 Current children cumulated CPU time (s) 658.89 Current children cumulated vsize (Kb) 120208 [startup+670.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36552 0 4 0 66719 142 0 0 25 0 1 0 1797849119 120946688 28689 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29528 28689 162 162 0 29366 0 [pid=22744] vsize: 118112 Current children cumulated CPU time (s) 668.89 Current children cumulated vsize (Kb) 120240 [startup+680.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36586 0 4 0 67719 142 0 0 25 0 1 0 1797849119 121212928 28723 4294967295 134512640 135167914 3221224432 3221223120 134566738 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29593 28723 162 162 0 29431 0 [pid=22744] vsize: 118372 Current children cumulated CPU time (s) 678.89 Current children cumulated vsize (Kb) 120500 [startup+690.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36587 0 4 0 68719 142 0 0 25 0 1 0 1797849119 121212928 28724 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29593 28724 162 162 0 29431 0 [pid=22744] vsize: 118372 Current children cumulated CPU time (s) 688.89 Current children cumulated vsize (Kb) 120500 [startup+700.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36588 0 4 0 69719 142 0 0 25 0 1 0 1797849119 121212928 28725 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29593 28725 162 162 0 29431 0 [pid=22744] vsize: 118372 Current children cumulated CPU time (s) 698.89 Current children cumulated vsize (Kb) 120500 [startup+710.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36589 0 4 0 70720 142 0 0 25 0 1 0 1797849119 121212928 28726 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29593 28726 162 162 0 29431 0 [pid=22744] vsize: 118372 Current children cumulated CPU time (s) 708.9 Current children cumulated vsize (Kb) 120500 [startup+720.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36592 0 4 0 71720 142 0 0 25 0 1 0 1797849119 121221120 28729 4294967295 134512640 135167914 3221224432 3221223092 134567766 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29595 28729 162 162 0 29433 0 [pid=22744] vsize: 118380 Current children cumulated CPU time (s) 718.9 Current children cumulated vsize (Kb) 120508 [startup+730.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36600 0 4 0 72720 142 0 0 25 0 1 0 1797849119 121253888 28737 4294967295 134512640 135167914 3221224432 3221223168 134559379 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29603 28737 162 162 0 29441 0 [pid=22744] vsize: 118412 Current children cumulated CPU time (s) 728.9 Current children cumulated vsize (Kb) 120540 [startup+740.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36608 0 4 0 73720 142 0 0 25 0 1 0 1797849119 121282560 28745 4294967295 134512640 135167914 3221224432 3221223168 134559387 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29610 28745 162 162 0 29448 0 [pid=22744] vsize: 118440 Current children cumulated CPU time (s) 738.9 Current children cumulated vsize (Kb) 120568 [startup+750.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36618 0 4 0 74720 143 0 0 25 0 1 0 1797849119 121319424 28755 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29619 28755 162 162 0 29457 0 [pid=22744] vsize: 118476 Current children cumulated CPU time (s) 748.91 Current children cumulated vsize (Kb) 120604 [startup+760.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36625 0 4 0 75720 143 0 0 25 0 1 0 1797849119 121344000 28762 4294967295 134512640 135167914 3221224432 3221223092 134567777 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29625 28762 162 162 0 29463 0 [pid=22744] vsize: 118500 Current children cumulated CPU time (s) 758.91 Current children cumulated vsize (Kb) 120628 [startup+770.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36631 0 4 0 76720 143 0 0 25 0 1 0 1797849119 121364480 28768 4294967295 134512640 135167914 3221224432 3221223120 134566713 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29630 28768 162 162 0 29468 0 [pid=22744] vsize: 118520 Current children cumulated CPU time (s) 768.91 Current children cumulated vsize (Kb) 120648 [startup+780.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36638 0 4 0 77720 143 0 0 25 0 1 0 1797849119 121393152 28775 4294967295 134512640 135167914 3221224432 3221223120 134566766 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29637 28775 162 162 0 29475 0 [pid=22744] vsize: 118548 Current children cumulated CPU time (s) 778.91 Current children cumulated vsize (Kb) 120676 [startup+790.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36648 0 4 0 78720 143 0 0 25 0 1 0 1797849119 121430016 28785 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29646 28785 162 162 0 29484 0 [pid=22744] vsize: 118584 Current children cumulated CPU time (s) 788.91 Current children cumulated vsize (Kb) 120712 [startup+800.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36655 0 4 0 79720 143 0 0 25 0 1 0 1797849119 121454592 28792 4294967295 134512640 135167914 3221224432 3221223120 134566741 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29652 28792 162 162 0 29490 0 [pid=22744] vsize: 118608 Current children cumulated CPU time (s) 798.91 Current children cumulated vsize (Kb) 120736 [startup+810.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36663 0 4 0 80720 143 0 0 25 0 1 0 1797849119 121483264 28800 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29659 28800 162 162 0 29497 0 [pid=22744] vsize: 118636 Current children cumulated CPU time (s) 808.91 Current children cumulated vsize (Kb) 120764 [startup+820.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36672 0 4 0 81720 143 0 0 25 0 1 0 1797849119 121520128 28809 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29668 28809 162 162 0 29506 0 [pid=22744] vsize: 118672 Current children cumulated CPU time (s) 818.91 Current children cumulated vsize (Kb) 120800 [startup+830.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36684 0 4 0 82720 143 0 0 25 0 1 0 1797849119 121565184 28821 4294967295 134512640 135167914 3221224432 3221223168 134559365 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29679 28821 162 162 0 29517 0 [pid=22744] vsize: 118716 Current children cumulated CPU time (s) 828.91 Current children cumulated vsize (Kb) 120844 [startup+840.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36692 0 4 0 83720 144 0 0 25 0 1 0 1797849119 121593856 28829 4294967295 134512640 135167914 3221224432 3221223136 134562669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29686 28829 162 162 0 29524 0 [pid=22744] vsize: 118744 Current children cumulated CPU time (s) 838.92 Current children cumulated vsize (Kb) 120872 [startup+850.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36699 0 4 0 84720 144 0 0 25 0 1 0 1797849119 121618432 28836 4294967295 134512640 135167914 3221224432 3221223092 134567777 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29692 28836 162 162 0 29530 0 [pid=22744] vsize: 118768 Current children cumulated CPU time (s) 848.92 Current children cumulated vsize (Kb) 120896 [startup+860.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36710 0 4 0 85720 144 0 0 25 0 1 0 1797849119 121659392 28847 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29702 28847 162 162 0 29540 0 [pid=22744] vsize: 118808 Current children cumulated CPU time (s) 858.92 Current children cumulated vsize (Kb) 120936 [startup+870.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36721 0 4 0 86720 144 0 0 25 0 1 0 1797849119 121700352 28858 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29712 28858 162 162 0 29550 0 [pid=22744] vsize: 118848 Current children cumulated CPU time (s) 868.92 Current children cumulated vsize (Kb) 120976 [startup+880.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36727 0 4 0 87721 144 0 0 25 0 1 0 1797849119 121724928 28864 4294967295 134512640 135167914 3221224432 3221223136 134566404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29718 28864 162 162 0 29556 0 [pid=22744] vsize: 118872 Current children cumulated CPU time (s) 878.93 Current children cumulated vsize (Kb) 121000 [startup+890.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36734 0 4 0 88721 144 0 0 25 0 1 0 1797849119 121749504 28871 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29724 28871 162 162 0 29562 0 [pid=22744] vsize: 118896 Current children cumulated CPU time (s) 888.93 Current children cumulated vsize (Kb) 121024 [startup+900.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36747 0 4 0 89721 144 0 0 25 0 1 0 1797849119 121798656 28884 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29736 28884 162 162 0 29574 0 [pid=22744] vsize: 118944 Current children cumulated CPU time (s) 898.93 Current children cumulated vsize (Kb) 121072 [startup+910.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36754 0 4 0 90721 144 0 0 25 0 1 0 1797849119 121827328 28891 4294967295 134512640 135167914 3221224432 3221223220 134563911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29743 28891 162 162 0 29581 0 [pid=22744] vsize: 118972 Current children cumulated CPU time (s) 908.93 Current children cumulated vsize (Kb) 121100 [startup+920.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36760 0 4 0 91721 144 0 0 25 0 1 0 1797849119 121847808 28897 4294967295 134512640 135167914 3221224432 3221223092 134567680 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29748 28897 162 162 0 29586 0 [pid=22744] vsize: 118992 Current children cumulated CPU time (s) 918.93 Current children cumulated vsize (Kb) 121120 [startup+930.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36770 0 4 0 92721 144 0 0 25 0 1 0 1797849119 121884672 28907 4294967295 134512640 135167914 3221224432 3221223168 134559332 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29757 28907 162 162 0 29595 0 [pid=22744] vsize: 119028 Current children cumulated CPU time (s) 928.93 Current children cumulated vsize (Kb) 121156 [startup+940.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36783 0 4 0 93721 144 0 0 25 0 1 0 1797849119 121933824 28920 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29769 28920 162 162 0 29607 0 [pid=22744] vsize: 119076 Current children cumulated CPU time (s) 938.93 Current children cumulated vsize (Kb) 121204 [startup+950.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36790 0 4 0 94722 144 0 0 25 0 1 0 1797849119 121962496 28927 4294967295 134512640 135167914 3221224432 3221223136 134566167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29776 28927 162 162 0 29614 0 [pid=22744] vsize: 119104 Current children cumulated CPU time (s) 948.94 Current children cumulated vsize (Kb) 121232 [startup+960.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36797 0 4 0 95722 144 0 0 25 0 1 0 1797849119 121987072 28934 4294967295 134512640 135167914 3221224432 3221223104 134562347 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29782 28934 162 162 0 29620 0 [pid=22744] vsize: 119128 Current children cumulated CPU time (s) 958.94 Current children cumulated vsize (Kb) 121256 [startup+970.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36809 0 4 0 96722 144 0 0 25 0 1 0 1797849119 122032128 28946 4294967295 134512640 135167914 3221224432 3221223136 134562682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29793 28946 162 162 0 29631 0 [pid=22744] vsize: 119172 Current children cumulated CPU time (s) 968.94 Current children cumulated vsize (Kb) 121300 [startup+980.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36825 0 4 0 97722 144 0 0 25 0 1 0 1797849119 122093568 28962 4294967295 134512640 135167914 3221224432 3221223092 134567680 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29808 28962 162 162 0 29646 0 [pid=22744] vsize: 119232 Current children cumulated CPU time (s) 978.94 Current children cumulated vsize (Kb) 121360 [startup+990.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36850 0 4 0 98721 145 0 0 25 0 1 0 1797849119 122191872 28987 4294967295 134512640 135167914 3221224432 3221223104 134566760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29832 28987 162 162 0 29670 0 [pid=22744] vsize: 119328 Current children cumulated CPU time (s) 988.94 Current children cumulated vsize (Kb) 121456 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36859 0 4 0 99721 145 0 0 25 0 1 0 1797849119 122228736 28996 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29841 28996 162 162 0 29679 0 [pid=22744] vsize: 119364 Current children cumulated CPU time (s) 998.94 Current children cumulated vsize (Kb) 121492 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36873 0 4 0 100721 145 0 0 25 0 1 0 1797849119 122281984 29010 4294967295 134512640 135167914 3221224432 3221223132 134566190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29854 29010 162 162 0 29692 0 [pid=22744] vsize: 119416 Current children cumulated CPU time (s) 1008.94 Current children cumulated vsize (Kb) 121544 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36887 0 4 0 101721 145 0 0 25 0 1 0 1797849119 122335232 29024 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29867 29024 162 162 0 29705 0 [pid=22744] vsize: 119468 Current children cumulated CPU time (s) 1018.94 Current children cumulated vsize (Kb) 121596 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36902 0 4 0 102721 145 0 0 25 0 1 0 1797849119 122392576 29039 4294967295 134512640 135167914 3221224432 3221223136 134566158 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29881 29039 162 162 0 29719 0 [pid=22744] vsize: 119524 Current children cumulated CPU time (s) 1028.94 Current children cumulated vsize (Kb) 121652 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36913 0 4 0 103721 145 0 0 25 0 1 0 1797849119 122433536 29050 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29891 29050 162 162 0 29729 0 [pid=22744] vsize: 119564 Current children cumulated CPU time (s) 1038.94 Current children cumulated vsize (Kb) 121692 [startup+1050.07 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36924 0 4 0 104721 145 0 0 25 0 1 0 1797849119 122478592 29061 4294967295 134512640 135167914 3221224432 3221223136 134562604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29902 29061 162 162 0 29740 0 [pid=22744] vsize: 119608 Current children cumulated CPU time (s) 1048.94 Current children cumulated vsize (Kb) 121736 [startup+1060.07 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36937 0 4 0 105721 145 0 0 25 0 1 0 1797849119 122527744 29074 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29914 29074 162 162 0 29752 0 [pid=22744] vsize: 119656 Current children cumulated CPU time (s) 1058.94 Current children cumulated vsize (Kb) 121784 [startup+1070.07 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36949 0 4 0 106721 145 0 0 25 0 1 0 1797849119 122572800 29086 4294967295 134512640 135167914 3221224432 3221223136 134566242 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 29925 29086 162 162 0 29763 0 [pid=22744] vsize: 119700 Current children cumulated CPU time (s) 1068.94 Current children cumulated vsize (Kb) 121828 [startup+1080.07 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36963 0 4 0 107721 145 0 0 25 0 1 0 1797849119 122888192 29100 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30002 29100 162 162 0 29840 0 [pid=22744] vsize: 120008 Current children cumulated CPU time (s) 1078.94 Current children cumulated vsize (Kb) 122136 [startup+1090.07 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36974 0 4 0 108721 145 0 0 25 0 1 0 1797849119 122933248 29111 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30013 29111 162 162 0 29851 0 [pid=22744] vsize: 120052 Current children cumulated CPU time (s) 1088.94 Current children cumulated vsize (Kb) 122180 [startup+1100.07 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36986 0 4 0 109721 145 0 0 25 0 1 0 1797849119 122978304 29123 4294967295 134512640 135167914 3221224432 3221223112 134562294 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30024 29123 162 162 0 29862 0 [pid=22744] vsize: 120096 Current children cumulated CPU time (s) 1098.94 Current children cumulated vsize (Kb) 122224 [startup+1110.07 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37003 0 4 0 110722 145 0 0 25 0 1 0 1797849119 123043840 29140 4294967295 134512640 135167914 3221224432 3221223120 134566795 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30040 29140 162 162 0 29878 0 [pid=22744] vsize: 120160 Current children cumulated CPU time (s) 1108.95 Current children cumulated vsize (Kb) 122288 [startup+1120.08 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37012 0 4 0 111722 145 0 0 25 0 1 0 1797849119 123076608 29149 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30048 29149 162 162 0 29886 0 [pid=22744] vsize: 120192 Current children cumulated CPU time (s) 1118.95 Current children cumulated vsize (Kb) 122320 [startup+1130.08 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37024 0 4 0 112722 146 0 0 25 0 1 0 1797849119 123125760 29161 4294967295 134512640 135167914 3221224432 3221223136 134562869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30060 29161 162 162 0 29898 0 [pid=22744] vsize: 120240 Current children cumulated CPU time (s) 1128.96 Current children cumulated vsize (Kb) 122368 [startup+1140.08 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37044 0 4 0 113721 146 0 0 25 0 1 0 1797849119 123203584 29181 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30079 29181 162 162 0 29917 0 [pid=22744] vsize: 120316 Current children cumulated CPU time (s) 1138.95 Current children cumulated vsize (Kb) 122444 [startup+1150.08 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37056 0 4 0 114721 146 0 0 25 0 1 0 1797849119 123248640 29193 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30090 29193 162 162 0 29928 0 [pid=22744] vsize: 120360 Current children cumulated CPU time (s) 1148.95 Current children cumulated vsize (Kb) 122488 [startup+1160.08 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37067 0 4 0 115722 146 0 0 25 0 1 0 1797849119 123289600 29204 4294967295 134512640 135167914 3221224432 3221223092 134567760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30100 29204 162 162 0 29938 0 [pid=22744] vsize: 120400 Current children cumulated CPU time (s) 1158.96 Current children cumulated vsize (Kb) 122528 [startup+1170.08 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37083 0 4 0 116721 146 0 0 25 0 1 0 1797849119 123351040 29220 4294967295 134512640 135167914 3221224432 3221223136 134562502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30115 29220 162 162 0 29953 0 [pid=22744] vsize: 120460 Current children cumulated CPU time (s) 1168.95 Current children cumulated vsize (Kb) 122588 [startup+1180.08 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37104 0 4 0 117721 146 0 0 25 0 1 0 1797849119 123432960 29241 4294967295 134512640 135167914 3221224432 3221223168 134559387 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30135 29241 162 162 0 29973 0 [pid=22744] vsize: 120540 Current children cumulated CPU time (s) 1178.95 Current children cumulated vsize (Kb) 122668 [startup+1190.08 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37121 0 4 0 118721 146 0 0 25 0 1 0 1797849119 123502592 29258 4294967295 134512640 135167914 3221224432 3221223092 134567699 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30152 29258 162 162 0 29990 0 [pid=22744] vsize: 120608 Current children cumulated CPU time (s) 1188.95 Current children cumulated vsize (Kb) 122736 [startup+1200.08 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37137 0 4 0 119721 146 0 0 25 0 1 0 1797849119 123564032 29274 4294967295 134512640 135167914 3221224432 3221223092 134567699 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30167 29274 162 162 0 30005 0 [pid=22744] vsize: 120668 Current children cumulated CPU time (s) 1198.95 Current children cumulated vsize (Kb) 122796 [startup+1210.08 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37156 0 4 0 120721 147 0 0 25 0 1 0 1797849119 123637760 29293 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30185 29293 162 162 0 30023 0 [pid=22744] vsize: 120740 Current children cumulated CPU time (s) 1208.96 Current children cumulated vsize (Kb) 122868 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 22744 Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22739/statm): 532 234 485 147 0 385 0 [pid=22739] vsize: 2128 Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37156 0 4 0 120721 147 0 0 25 0 1 0 1797849119 123637760 29293 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22744/statm): 30185 29293 162 162 0 30023 0 [pid=22744] vsize: 120740 Current children cumulated CPU time (s) 1208.96 Current children cumulated vsize (Kb) 122868 Sending SIGTERM to -22739 Sleeping 2 seconds One traced child (pid=22739) ended because it received signal 15 (SIGTERM) One traced child (pid=22744) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1208.74 CPU user time (s): 1207.21 CPU system time (s): 1.52477 CPU usage (%): 99.8842 Max. virtual memory (cumulated for all children) (Kb): 122868
ERROR: no interpretation found !