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/32124/stat): 32124 (minisat+_script) R 32123 32124 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846790871 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/32124/statm): 174 3 169 147 0 27 0
[pid=32124] 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=32125
New process pid=32126
New process pid=32127
execve syscall for /bin/sed executable
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
One traced child (pid=32126) exited with status: 0
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=32127) exited with status: 0
One traced child (pid=32125) exited with status: 0
New process pid=32128
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-pp08a.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8399 0 0 0 928 35 0 0 25 0 1 0 1846790876 36700160 8030 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 8960 8030 145 145 0 8815 0
[pid=32128] vsize: 35840
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 37964

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8422 0 0 0 1927 36 0 0 25 0 1 0 1846790876 36769792 8053 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 8977 8053 145 145 0 8832 0
[pid=32128] vsize: 35908
Current children cumulated CPU time (s) 19.64
Current children cumulated vsize (Kb) 38032

[startup+30.006 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8455 0 0 0 2925 36 0 0 25 0 1 0 1846790876 36884480 8086 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9005 8086 145 145 0 8860 0
[pid=32128] vsize: 36020
Current children cumulated CPU time (s) 29.62
Current children cumulated vsize (Kb) 38144

[startup+40.0067 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8486 0 0 0 3925 37 0 0 25 0 1 0 1846790876 36982784 8117 4294967295 134512640 135094434 3221224432 3221223136 134559007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9029 8117 145 145 0 8884 0
[pid=32128] vsize: 36116
Current children cumulated CPU time (s) 39.63
Current children cumulated vsize (Kb) 38240

[startup+50.0074 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8522 0 0 0 4924 37 0 0 25 0 1 0 1846790876 37130240 8153 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9065 8153 145 145 0 8920 0
[pid=32128] vsize: 36260
Current children cumulated CPU time (s) 49.62
Current children cumulated vsize (Kb) 38384

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8558 0 0 0 5923 38 0 0 25 0 1 0 1846790876 37249024 8189 4294967295 134512640 135094434 3221224432 3221223100 134553522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9094 8189 145 145 0 8949 0
[pid=32128] vsize: 36376
Current children cumulated CPU time (s) 59.62
Current children cumulated vsize (Kb) 38500

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8585 0 0 0 6923 38 0 0 25 0 1 0 1846790876 37355520 8216 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9120 8216 145 145 0 8975 0
[pid=32128] vsize: 36480
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 38604

[startup+80.0095 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8611 0 0 0 7921 39 0 0 25 0 1 0 1846790876 37498880 8242 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 9155 8242 145 145 0 9010 0
[pid=32128] vsize: 36620
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 38744

[startup+90.0102 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8643 0 0 0 8919 40 0 0 25 0 1 0 1846790876 37605376 8274 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 9181 8274 145 145 0 9036 0
[pid=32128] vsize: 36724
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 38848

[startup+100.011 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8662 0 0 0 9919 40 0 0 25 0 1 0 1846790876 37666816 8293 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 9196 8293 145 145 0 9051 0
[pid=32128] vsize: 36784
Current children cumulated CPU time (s) 99.6
Current children cumulated vsize (Kb) 38908

[startup+110.013 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8682 0 0 0 10918 41 0 0 25 0 1 0 1846790876 37740544 8313 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 9214 8313 145 145 0 9069 0
[pid=32128] vsize: 36856
Current children cumulated CPU time (s) 109.6
Current children cumulated vsize (Kb) 38980

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8707 0 0 0 11917 41 0 0 25 0 1 0 1846790876 37834752 8338 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 9237 8338 145 145 0 9092 0
[pid=32128] vsize: 36948
Current children cumulated CPU time (s) 119.59
Current children cumulated vsize (Kb) 39072

[startup+130.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8733 0 0 0 12917 41 0 0 25 0 1 0 1846790876 37920768 8364 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9258 8364 145 145 0 9113 0
[pid=32128] vsize: 37032
Current children cumulated CPU time (s) 129.59
Current children cumulated vsize (Kb) 39156

[startup+140.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8763 0 0 0 13916 42 0 0 25 0 1 0 1846790876 38031360 8394 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9285 8394 145 145 0 9140 0
[pid=32128] vsize: 37140
Current children cumulated CPU time (s) 139.59
Current children cumulated vsize (Kb) 39264

[startup+150.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8812 0 0 0 14916 42 0 0 25 0 1 0 1846790876 38359040 8443 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9365 8443 145 145 0 9220 0
[pid=32128] vsize: 37460
Current children cumulated CPU time (s) 149.59
Current children cumulated vsize (Kb) 39584

[startup+160.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8817 0 0 0 15916 42 0 0 25 0 1 0 1846790876 38367232 8448 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9367 8448 145 145 0 9222 0
[pid=32128] vsize: 37468
Current children cumulated CPU time (s) 159.59
Current children cumulated vsize (Kb) 39592

[startup+170.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8847 0 0 0 16915 42 0 0 25 0 1 0 1846790876 38477824 8478 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9394 8478 145 145 0 9249 0
[pid=32128] vsize: 37576
Current children cumulated CPU time (s) 169.58
Current children cumulated vsize (Kb) 39700

[startup+180.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8869 0 0 0 17915 42 0 0 25 0 1 0 1846790876 38559744 8500 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9414 8500 145 145 0 9269 0
[pid=32128] vsize: 37656
Current children cumulated CPU time (s) 179.58
Current children cumulated vsize (Kb) 39780

[startup+190.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8897 0 0 0 18915 43 0 0 25 0 1 0 1846790876 38666240 8528 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9440 8528 145 145 0 9295 0
[pid=32128] vsize: 37760
Current children cumulated CPU time (s) 189.59
Current children cumulated vsize (Kb) 39884

[startup+200.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8927 0 0 0 19915 43 0 0 25 0 1 0 1846790876 38780928 8558 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9468 8558 145 145 0 9323 0
[pid=32128] vsize: 37872
Current children cumulated CPU time (s) 199.59
Current children cumulated vsize (Kb) 39996

[startup+210.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8964 0 0 0 20914 43 0 0 25 0 1 0 1846790876 38916096 8595 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9501 8595 145 145 0 9356 0
[pid=32128] vsize: 38004
Current children cumulated CPU time (s) 209.58
Current children cumulated vsize (Kb) 40128

[startup+220.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 8996 0 0 0 21913 44 0 0 25 0 1 0 1846790876 39030784 8627 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9529 8627 145 145 0 9384 0
[pid=32128] vsize: 38116
Current children cumulated CPU time (s) 219.58
Current children cumulated vsize (Kb) 40240

[startup+230.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9023 0 0 0 22913 44 0 0 25 0 1 0 1846790876 39133184 8654 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9554 8654 145 145 0 9409 0
[pid=32128] vsize: 38216
Current children cumulated CPU time (s) 229.58
Current children cumulated vsize (Kb) 40340

[startup+240.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9048 0 0 0 23913 44 0 0 25 0 1 0 1846790876 39227392 8679 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9577 8679 145 145 0 9432 0
[pid=32128] vsize: 38308
Current children cumulated CPU time (s) 239.58
Current children cumulated vsize (Kb) 40432

[startup+250.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9070 0 0 0 24912 45 0 0 25 0 1 0 1846790876 39309312 8701 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9597 8701 145 145 0 9452 0
[pid=32128] vsize: 38388
Current children cumulated CPU time (s) 249.58
Current children cumulated vsize (Kb) 40512

[startup+260.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9101 0 0 0 25912 45 0 0 25 0 1 0 1846790876 39424000 8732 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9625 8732 145 145 0 9480 0
[pid=32128] vsize: 38500
Current children cumulated CPU time (s) 259.58
Current children cumulated vsize (Kb) 40624

[startup+270.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9134 0 0 0 26912 45 0 0 25 0 1 0 1846790876 39538688 8765 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9653 8765 145 145 0 9508 0
[pid=32128] vsize: 38612
Current children cumulated CPU time (s) 269.58
Current children cumulated vsize (Kb) 40736

[startup+280.027 s]
Raw data (loadavg): 0.99 0.98 0.99 3/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9190 0 0 0 27911 46 0 0 25 0 1 0 1846790876 39755776 8821 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9706 8821 145 145 0 9561 0
[pid=32128] vsize: 38824
Current children cumulated CPU time (s) 279.58
Current children cumulated vsize (Kb) 40948

[startup+290.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9215 0 0 0 28911 46 0 0 25 0 1 0 1846790876 39849984 8846 4294967295 134512640 135094434 3221224432 3221223044 134563132 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9729 8846 145 145 0 9584 0
[pid=32128] vsize: 38916
Current children cumulated CPU time (s) 289.58
Current children cumulated vsize (Kb) 41040

[startup+300.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9246 0 0 0 29911 46 0 0 25 0 1 0 1846790876 40230912 8877 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9822 8877 145 145 0 9677 0
[pid=32128] vsize: 39288
Current children cumulated CPU time (s) 299.58
Current children cumulated vsize (Kb) 41412

[startup+310.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9290 0 0 0 30910 46 0 0 25 0 1 0 1846790876 40398848 8921 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9863 8921 145 145 0 9718 0
[pid=32128] vsize: 39452
Current children cumulated CPU time (s) 309.57
Current children cumulated vsize (Kb) 41576

[startup+320.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9338 0 0 0 31909 47 0 0 25 0 1 0 1846790876 40583168 8969 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9908 8969 145 145 0 9763 0
[pid=32128] vsize: 39632
Current children cumulated CPU time (s) 319.57
Current children cumulated vsize (Kb) 41756

[startup+330.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9371 0 0 0 32909 47 0 0 25 0 1 0 1846790876 40710144 9002 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9939 9002 145 145 0 9794 0
[pid=32128] vsize: 39756
Current children cumulated CPU time (s) 329.57
Current children cumulated vsize (Kb) 41880

[startup+340.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9406 0 0 0 33907 48 0 0 25 0 1 0 1846790876 40845312 9037 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 9972 9037 145 145 0 9827 0
[pid=32128] vsize: 39888
Current children cumulated CPU time (s) 339.56
Current children cumulated vsize (Kb) 42012

[startup+350.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9448 0 0 0 34907 48 0 0 25 0 1 0 1846790876 41009152 9079 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10012 9079 145 145 0 9867 0
[pid=32128] vsize: 40048
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 42172

[startup+360.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9491 0 0 0 35906 49 0 0 25 0 1 0 1846790876 41172992 9122 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10052 9122 145 145 0 9907 0
[pid=32128] vsize: 40208
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 42332

[startup+370.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9527 0 0 0 36905 49 0 0 25 0 1 0 1846790876 41312256 9158 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10086 9158 145 145 0 9941 0
[pid=32128] vsize: 40344
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 42468

[startup+380.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9570 0 0 0 37905 49 0 0 25 0 1 0 1846790876 41480192 9201 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 10127 9201 145 145 0 9982 0
[pid=32128] vsize: 40508
Current children cumulated CPU time (s) 379.55
Current children cumulated vsize (Kb) 42632

[startup+390.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9616 0 0 0 38903 50 0 0 25 0 1 0 1846790876 41660416 9247 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10171 9247 145 145 0 10026 0
[pid=32128] vsize: 40684
Current children cumulated CPU time (s) 389.54
Current children cumulated vsize (Kb) 42808

[startup+400.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9658 0 0 0 39902 51 0 0 25 0 1 0 1846790876 41820160 9289 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10210 9289 145 145 0 10065 0
[pid=32128] vsize: 40840
Current children cumulated CPU time (s) 399.54
Current children cumulated vsize (Kb) 42964

[startup+410.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9693 0 0 0 40902 51 0 0 25 0 1 0 1846790876 41955328 9324 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10243 9324 145 145 0 10098 0
[pid=32128] vsize: 40972
Current children cumulated CPU time (s) 409.54
Current children cumulated vsize (Kb) 43096

[startup+420.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9729 0 0 0 41901 51 0 0 25 0 1 0 1846790876 42090496 9360 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10276 9360 145 145 0 10131 0
[pid=32128] vsize: 41104
Current children cumulated CPU time (s) 419.53
Current children cumulated vsize (Kb) 43228

[startup+430.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9797 0 0 0 42900 52 0 0 25 0 1 0 1846790876 42356736 9428 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10341 9428 145 145 0 10196 0
[pid=32128] vsize: 41364
Current children cumulated CPU time (s) 429.53
Current children cumulated vsize (Kb) 43488

[startup+440.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9841 0 0 0 43899 52 0 0 25 0 1 0 1846790876 42528768 9472 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10383 9472 145 145 0 10238 0
[pid=32128] vsize: 41532
Current children cumulated CPU time (s) 439.52
Current children cumulated vsize (Kb) 43656

[startup+450.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9890 0 0 0 44898 53 0 0 25 0 1 0 1846790876 42713088 9521 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10428 9521 145 145 0 10283 0
[pid=32128] vsize: 41712
Current children cumulated CPU time (s) 449.52
Current children cumulated vsize (Kb) 43836

[startup+460.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9938 0 0 0 45897 53 0 0 25 0 1 0 1846790876 42897408 9569 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10473 9569 145 145 0 10328 0
[pid=32128] vsize: 41892
Current children cumulated CPU time (s) 459.51
Current children cumulated vsize (Kb) 44016

[startup+470.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 9985 0 0 0 46896 54 0 0 25 0 1 0 1846790876 43081728 9616 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10518 9616 145 145 0 10373 0
[pid=32128] vsize: 42072
Current children cumulated CPU time (s) 469.51
Current children cumulated vsize (Kb) 44196

[startup+480.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 10025 0 0 0 47895 55 0 0 25 0 1 0 1846790876 43237376 9656 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10556 9656 145 145 0 10411 0
[pid=32128] vsize: 42224
Current children cumulated CPU time (s) 479.51
Current children cumulated vsize (Kb) 44348

[startup+490.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 10063 0 0 0 48894 55 0 0 25 0 1 0 1846790876 43384832 9694 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10592 9694 145 145 0 10447 0
[pid=32128] vsize: 42368
Current children cumulated CPU time (s) 489.5
Current children cumulated vsize (Kb) 44492

[startup+500.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 10181 0 0 0 49892 56 0 0 25 0 1 0 1846790876 43843584 9812 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 10704 9812 145 145 0 10559 0
[pid=32128] vsize: 42816
Current children cumulated CPU time (s) 499.49
Current children cumulated vsize (Kb) 44940

[startup+510.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 10252 0 0 0 50891 56 0 0 25 0 1 0 1846790876 44122112 9883 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 10772 9883 145 145 0 10627 0
[pid=32128] vsize: 43088
Current children cumulated CPU time (s) 509.48
Current children cumulated vsize (Kb) 45212

[startup+520.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 10524 0 0 0 51888 58 0 0 25 0 1 0 1846790876 45207552 10155 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 11037 10155 145 145 0 10892 0
[pid=32128] vsize: 44148
Current children cumulated CPU time (s) 519.47
Current children cumulated vsize (Kb) 46272

[startup+530.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 10722 0 0 0 52882 59 0 0 25 0 1 0 1846790876 46522368 10353 4294967295 134512640 135094434 3221224432 3221223024 134551989 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 11358 10353 145 145 0 11213 0
[pid=32128] vsize: 45432
Current children cumulated CPU time (s) 529.42
Current children cumulated vsize (Kb) 47556

[startup+540.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 10801 0 0 0 53880 61 0 0 25 0 1 0 1846790876 46833664 10432 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 11434 10432 145 145 0 11289 0
[pid=32128] vsize: 45736
Current children cumulated CPU time (s) 539.42
Current children cumulated vsize (Kb) 47860

[startup+550.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11003 0 0 0 54876 62 0 0 25 0 1 0 1846790876 47640576 10634 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 11631 10634 145 145 0 11486 0
[pid=32128] vsize: 46524
Current children cumulated CPU time (s) 549.39
Current children cumulated vsize (Kb) 48648

[startup+560.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11109 0 0 0 55874 63 0 0 25 0 1 0 1846790876 48058368 10740 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 11733 10740 145 145 0 11588 0
[pid=32128] vsize: 46932
Current children cumulated CPU time (s) 559.38
Current children cumulated vsize (Kb) 49056

[startup+570.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11229 0 0 0 56872 64 0 0 25 0 1 0 1846790876 48533504 10860 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 11849 10860 145 145 0 11704 0
[pid=32128] vsize: 47396
Current children cumulated CPU time (s) 569.37
Current children cumulated vsize (Kb) 49520

[startup+580.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11286 0 0 0 57871 65 0 0 25 0 1 0 1846790876 48758784 10917 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 11904 10917 145 145 0 11759 0
[pid=32128] vsize: 47616
Current children cumulated CPU time (s) 579.37
Current children cumulated vsize (Kb) 49740

[startup+590.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11344 0 0 0 58869 66 0 0 25 0 1 0 1846790876 48984064 10975 4294967295 134512640 135094434 3221224432 3221223044 134563107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 11959 10975 145 145 0 11814 0
[pid=32128] vsize: 47836
Current children cumulated CPU time (s) 589.36
Current children cumulated vsize (Kb) 49960

[startup+600.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11420 0 0 0 59867 67 0 0 25 0 1 0 1846790876 49283072 11051 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12032 11051 145 145 0 11887 0
[pid=32128] vsize: 48128
Current children cumulated CPU time (s) 599.35
Current children cumulated vsize (Kb) 50252

[startup+610.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11483 0 0 0 60866 68 0 0 25 0 1 0 1846790876 49528832 11114 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12092 11114 145 145 0 11947 0
[pid=32128] vsize: 48368
Current children cumulated CPU time (s) 609.35
Current children cumulated vsize (Kb) 50492

[startup+620.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11662 0 0 0 61863 70 0 0 25 0 1 0 1846790876 50245632 11293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12267 11293 145 145 0 12122 0
[pid=32128] vsize: 49068
Current children cumulated CPU time (s) 619.34
Current children cumulated vsize (Kb) 51192

[startup+630.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11744 0 0 0 62861 71 0 0 25 0 1 0 1846790876 50569216 11375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12346 11375 145 145 0 12201 0
[pid=32128] vsize: 49384
Current children cumulated CPU time (s) 629.33
Current children cumulated vsize (Kb) 51508

[startup+640.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11805 0 0 0 63860 73 0 0 25 0 1 0 1846790876 50810880 11436 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12405 11436 145 145 0 12260 0
[pid=32128] vsize: 49620
Current children cumulated CPU time (s) 639.34
Current children cumulated vsize (Kb) 51744

[startup+650.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 11922 0 0 0 64857 74 0 0 25 0 1 0 1846790876 51277824 11553 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12519 11553 145 145 0 12374 0
[pid=32128] vsize: 50076
Current children cumulated CPU time (s) 649.32
Current children cumulated vsize (Kb) 52200

[startup+660.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 12007 0 0 0 65856 74 0 0 25 0 1 0 1846790876 51609600 11638 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12600 11638 145 145 0 12455 0
[pid=32128] vsize: 50400
Current children cumulated CPU time (s) 659.31
Current children cumulated vsize (Kb) 52524

[startup+670.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 12062 0 0 0 66856 75 0 0 25 0 1 0 1846790876 51822592 11693 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12652 11693 145 145 0 12507 0
[pid=32128] vsize: 50608
Current children cumulated CPU time (s) 669.32
Current children cumulated vsize (Kb) 52732

[startup+680.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 12127 0 0 0 67854 76 0 0 25 0 1 0 1846790876 52076544 11758 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12714 11758 145 145 0 12569 0
[pid=32128] vsize: 50856
Current children cumulated CPU time (s) 679.31
Current children cumulated vsize (Kb) 52980

[startup+690.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 12240 0 0 0 68852 77 0 0 25 0 1 0 1846790876 52527104 11871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12824 11871 145 145 0 12679 0
[pid=32128] vsize: 51296
Current children cumulated CPU time (s) 689.3
Current children cumulated vsize (Kb) 53420

[startup+700.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 12315 0 0 0 69851 78 0 0 25 0 1 0 1846790876 52826112 11946 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12897 11946 145 145 0 12752 0
[pid=32128] vsize: 51588
Current children cumulated CPU time (s) 699.3
Current children cumulated vsize (Kb) 53712

[startup+710.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 12405 0 0 0 70849 79 0 0 25 0 1 0 1846790876 53182464 12036 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 12984 12036 145 145 0 12839 0
[pid=32128] vsize: 51936
Current children cumulated CPU time (s) 709.29
Current children cumulated vsize (Kb) 54060

[startup+720.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 12505 0 0 0 71846 80 0 0 25 0 1 0 1846790876 53579776 12136 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 13081 12136 145 145 0 12936 0
[pid=32128] vsize: 52324
Current children cumulated CPU time (s) 719.27
Current children cumulated vsize (Kb) 54448

[startup+730.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 12964 0 0 0 72837 83 0 0 25 0 1 0 1846790876 55422976 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 13531 12595 145 145 0 13386 0
[pid=32128] vsize: 54124
Current children cumulated CPU time (s) 729.21
Current children cumulated vsize (Kb) 56248

[startup+740.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13129 0 0 0 73834 85 0 0 25 0 1 0 1846790876 56086528 12760 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 13693 12760 145 145 0 13548 0
[pid=32128] vsize: 54772
Current children cumulated CPU time (s) 739.2
Current children cumulated vsize (Kb) 56896

[startup+750.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13344 0 0 0 74830 87 0 0 25 0 1 0 1846790876 56946688 12975 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 13903 12975 145 145 0 13758 0
[pid=32128] vsize: 55612
Current children cumulated CPU time (s) 749.18
Current children cumulated vsize (Kb) 57736

[startup+760.068 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) T 32124 32124 20728 0 -1 0 13415 0 0 0 75828 88 0 0 25 0 1 0 1846790876 57233408 13046 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32128/statm): 13973 13046 145 145 0 13828 0
[pid=32128] vsize: 55892
Current children cumulated CPU time (s) 759.17
Current children cumulated vsize (Kb) 58016

[startup+770.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13509 0 0 0 76827 89 0 0 25 0 1 0 1846790876 57593856 13140 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14061 13140 145 145 0 13916 0
[pid=32128] vsize: 56244
Current children cumulated CPU time (s) 769.17
Current children cumulated vsize (Kb) 58368

[startup+780.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13650 0 0 0 77824 90 0 0 25 0 1 0 1846790876 58155008 13281 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14198 13281 145 145 0 14053 0
[pid=32128] vsize: 56792
Current children cumulated CPU time (s) 779.15
Current children cumulated vsize (Kb) 58916

[startup+790.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13725 0 0 0 78822 91 0 0 25 0 1 0 1846790876 58454016 13356 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14271 13356 145 145 0 14126 0
[pid=32128] vsize: 57084
Current children cumulated CPU time (s) 789.14
Current children cumulated vsize (Kb) 59208

[startup+800.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13832 0 0 0 79821 91 0 0 25 0 1 0 1846790876 58875904 13463 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14374 13463 145 145 0 14229 0
[pid=32128] vsize: 57496
Current children cumulated CPU time (s) 799.13
Current children cumulated vsize (Kb) 59620

[startup+810.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13878 0 0 0 80821 91 0 0 25 0 1 0 1846790876 59060224 13509 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14419 13509 145 145 0 14274 0
[pid=32128] vsize: 57676
Current children cumulated CPU time (s) 809.13
Current children cumulated vsize (Kb) 59800

[startup+820.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13944 0 0 0 81819 93 0 0 25 0 1 0 1846790876 59322368 13575 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14483 13575 145 145 0 14338 0
[pid=32128] vsize: 57932
Current children cumulated CPU time (s) 819.13
Current children cumulated vsize (Kb) 60056

[startup+830.074 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 13992 0 0 0 82818 94 0 0 25 0 1 0 1846790876 59518976 13623 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14531 13623 145 145 0 14386 0
[pid=32128] vsize: 58124
Current children cumulated CPU time (s) 829.13
Current children cumulated vsize (Kb) 60248

[startup+840.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 14082 0 0 0 83817 94 0 0 25 0 1 0 1846790876 59879424 13713 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14619 13713 145 145 0 14474 0
[pid=32128] vsize: 58476
Current children cumulated CPU time (s) 839.12
Current children cumulated vsize (Kb) 60600

[startup+850.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 14171 0 0 0 84815 95 0 0 25 0 1 0 1846790876 60227584 13802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14704 13802 145 145 0 14559 0
[pid=32128] vsize: 58816
Current children cumulated CPU time (s) 849.11
Current children cumulated vsize (Kb) 60940

[startup+860.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 14263 0 0 0 85813 96 0 0 25 0 1 0 1846790876 60592128 13894 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14793 13894 145 145 0 14648 0
[pid=32128] vsize: 59172
Current children cumulated CPU time (s) 859.1
Current children cumulated vsize (Kb) 61296

[startup+870.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 14365 0 0 0 86812 97 0 0 25 0 1 0 1846790876 61001728 13996 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 14893 13996 145 145 0 14748 0
[pid=32128] vsize: 59572
Current children cumulated CPU time (s) 869.1
Current children cumulated vsize (Kb) 61696

[startup+880.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 14499 0 0 0 87809 98 0 0 25 0 1 0 1846790876 61534208 14130 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 15023 14130 145 145 0 14878 0
[pid=32128] vsize: 60092
Current children cumulated CPU time (s) 879.08
Current children cumulated vsize (Kb) 62216

[startup+890.08 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) T 32124 32124 20728 0 -1 0 14582 0 0 0 88808 99 0 0 25 0 1 0 1846790876 61870080 14213 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32128/statm): 15105 14213 145 145 0 14960 0
[pid=32128] vsize: 60420
Current children cumulated CPU time (s) 889.08
Current children cumulated vsize (Kb) 62544

[startup+900.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 14829 0 0 0 89804 100 0 0 25 0 1 0 1846790876 63938560 14460 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 15610 14460 145 145 0 15465 0
[pid=32128] vsize: 62440
Current children cumulated CPU time (s) 899.05
Current children cumulated vsize (Kb) 64564

[startup+910.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 14930 0 0 0 90803 100 0 0 25 0 1 0 1846790876 64344064 14561 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 15709 14561 145 145 0 15564 0
[pid=32128] vsize: 62836
Current children cumulated CPU time (s) 909.04
Current children cumulated vsize (Kb) 64960

[startup+920.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 14992 0 0 0 91802 101 0 0 25 0 1 0 1846790876 64585728 14623 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 15768 14623 145 145 0 15623 0
[pid=32128] vsize: 63072
Current children cumulated CPU time (s) 919.04
Current children cumulated vsize (Kb) 65196

[startup+930.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 15079 0 0 0 92800 102 0 0 25 0 1 0 1846790876 64942080 14710 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 15855 14710 145 145 0 15710 0
[pid=32128] vsize: 63420
Current children cumulated CPU time (s) 929.03
Current children cumulated vsize (Kb) 65544

[startup+940.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 15173 0 0 0 93799 103 0 0 25 0 1 0 1846790876 65314816 14804 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 15946 14804 145 145 0 15801 0
[pid=32128] vsize: 63784
Current children cumulated CPU time (s) 939.03
Current children cumulated vsize (Kb) 65908

[startup+950.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 15417 0 0 0 94795 105 0 0 25 0 1 0 1846790876 66281472 15048 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 16182 15048 145 145 0 16037 0
[pid=32128] vsize: 64728
Current children cumulated CPU time (s) 949.01
Current children cumulated vsize (Kb) 66852

[startup+960.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 15702 0 0 0 95789 107 0 0 25 0 1 0 1846790876 67432448 15333 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32128/statm): 16463 15333 145 145 0 16318 0
[pid=32128] vsize: 65852
Current children cumulated CPU time (s) 958.97
Current children cumulated vsize (Kb) 67976

[startup+970.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 15867 0 0 0 96785 109 0 0 25 0 1 0 1846790876 68091904 15498 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 16624 15498 145 145 0 16479 0
[pid=32128] vsize: 66496
Current children cumulated CPU time (s) 968.95
Current children cumulated vsize (Kb) 68620

[startup+980.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 16056 0 0 0 97780 111 0 0 25 0 1 0 1846790876 68849664 15687 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 16809 15687 145 145 0 16664 0
[pid=32128] vsize: 67236
Current children cumulated CPU time (s) 978.92
Current children cumulated vsize (Kb) 69360

[startup+990.089 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 16180 0 0 0 98778 112 0 0 25 0 1 0 1846790876 69345280 15811 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 16930 15811 145 145 0 16785 0
[pid=32128] vsize: 67720
Current children cumulated CPU time (s) 988.91
Current children cumulated vsize (Kb) 69844

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 16313 0 0 0 99776 114 0 0 25 0 1 0 1846790876 69865472 15944 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 17057 15944 145 145 0 16912 0
[pid=32128] vsize: 68228
Current children cumulated CPU time (s) 998.91
Current children cumulated vsize (Kb) 70352

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 16493 0 0 0 100772 116 0 0 25 0 1 0 1846790876 70578176 16124 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 17231 16124 145 145 0 17086 0
[pid=32128] vsize: 68924
Current children cumulated CPU time (s) 1008.89
Current children cumulated vsize (Kb) 71048

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 16581 0 0 0 101770 117 0 0 25 0 1 0 1846790876 70930432 16212 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 17317 16212 145 145 0 17172 0
[pid=32128] vsize: 69268
Current children cumulated CPU time (s) 1018.88
Current children cumulated vsize (Kb) 71392

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 16759 0 0 0 102768 118 0 0 25 0 1 0 1846790876 71630848 16390 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 17488 16390 145 145 0 17343 0
[pid=32128] vsize: 69952
Current children cumulated CPU time (s) 1028.87
Current children cumulated vsize (Kb) 72076

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 16937 0 0 0 103764 119 0 0 25 0 1 0 1846790876 72351744 16568 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 17664 16568 145 145 0 17519 0
[pid=32128] vsize: 70656
Current children cumulated CPU time (s) 1038.84
Current children cumulated vsize (Kb) 72780

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 17277 0 0 0 104758 122 0 0 25 0 1 0 1846790876 73715712 16908 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 17997 16908 145 145 0 17852 0
[pid=32128] vsize: 71988
Current children cumulated CPU time (s) 1048.81
Current children cumulated vsize (Kb) 74112

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 17698 0 0 0 105752 125 0 0 25 0 1 0 1846790876 75411456 17329 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 18411 17329 145 145 0 18266 0
[pid=32128] vsize: 73644
Current children cumulated CPU time (s) 1058.78
Current children cumulated vsize (Kb) 75768

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 17928 0 0 0 106748 127 0 0 25 0 1 0 1846790876 76353536 17559 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 18641 17559 145 145 0 18496 0
[pid=32128] vsize: 74564
Current children cumulated CPU time (s) 1068.76
Current children cumulated vsize (Kb) 76688

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 18099 0 0 0 107745 128 0 0 25 0 1 0 1846790876 77037568 17730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 18808 17730 145 145 0 18663 0
[pid=32128] vsize: 75232
Current children cumulated CPU time (s) 1078.74
Current children cumulated vsize (Kb) 77356

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 18297 0 0 0 108741 130 0 0 25 0 1 0 1846790876 77824000 17928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19000 17928 145 145 0 18855 0
[pid=32128] vsize: 76000
Current children cumulated CPU time (s) 1088.72
Current children cumulated vsize (Kb) 78124

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 18444 0 0 0 109739 131 0 0 25 0 1 0 1846790876 78405632 18075 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19142 18075 145 145 0 18997 0
[pid=32128] vsize: 76568
Current children cumulated CPU time (s) 1098.71
Current children cumulated vsize (Kb) 78692

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 18550 0 0 0 110737 131 0 0 25 0 1 0 1846790876 78827520 18181 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19245 18181 145 145 0 19100 0
[pid=32128] vsize: 76980
Current children cumulated CPU time (s) 1108.69
Current children cumulated vsize (Kb) 79104

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 18617 0 0 0 111736 132 0 0 25 0 1 0 1846790876 79089664 18248 4294967295 134512640 135094434 3221224432 3221223044 134563030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19309 18248 145 145 0 19164 0
[pid=32128] vsize: 77236
Current children cumulated CPU time (s) 1118.69
Current children cumulated vsize (Kb) 79360

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 18696 0 0 0 112734 133 0 0 25 0 1 0 1846790876 79413248 18327 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19388 18327 145 145 0 19243 0
[pid=32128] vsize: 77552
Current children cumulated CPU time (s) 1128.68
Current children cumulated vsize (Kb) 79676

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 18828 0 0 0 113732 134 0 0 25 0 1 0 1846790876 79958016 18459 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19521 18459 145 145 0 19376 0
[pid=32128] vsize: 78084
Current children cumulated CPU time (s) 1138.67
Current children cumulated vsize (Kb) 80208

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 19026 0 0 0 114730 135 0 0 25 0 1 0 1846790876 80760832 18657 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19717 18657 145 145 0 19572 0
[pid=32128] vsize: 78868
Current children cumulated CPU time (s) 1148.66
Current children cumulated vsize (Kb) 80992

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 19175 0 0 0 115727 136 0 0 25 0 1 0 1846790876 81354752 18806 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19862 18806 145 145 0 19717 0
[pid=32128] vsize: 79448
Current children cumulated CPU time (s) 1158.64
Current children cumulated vsize (Kb) 81572

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 19251 0 0 0 116725 137 0 0 25 0 1 0 1846790876 81649664 18882 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 19934 18882 145 145 0 19789 0
[pid=32128] vsize: 79736
Current children cumulated CPU time (s) 1168.63
Current children cumulated vsize (Kb) 81860

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) T 32124 32124 20728 0 -1 0 19371 0 0 0 117723 138 0 0 25 0 1 0 1846790876 82132992 19002 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32128/statm): 20052 19002 145 145 0 19907 0
[pid=32128] vsize: 80208
Current children cumulated CPU time (s) 1178.62
Current children cumulated vsize (Kb) 82332

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) T 32124 32124 20728 0 -1 0 19449 0 0 0 118721 140 0 0 25 0 1 0 1846790876 82436096 19080 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32128/statm): 20126 19080 145 145 0 19981 0
[pid=32128] vsize: 80504
Current children cumulated CPU time (s) 1188.62
Current children cumulated vsize (Kb) 82628

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 19563 0 0 0 119718 142 0 0 25 0 1 0 1846790876 82903040 19194 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 20240 19194 145 145 0 20095 0
[pid=32128] vsize: 80960
Current children cumulated CPU time (s) 1198.61
Current children cumulated vsize (Kb) 83084

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 19700 0 0 0 120715 143 0 0 25 0 1 0 1846790876 83451904 19331 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 20374 19331 145 145 0 20229 0
[pid=32128] vsize: 81496
Current children cumulated CPU time (s) 1208.59
Current children cumulated vsize (Kb) 83620



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 32128
Raw data (/proc/32124/stat): 32124 (minisat+_script) S 32123 32124 20728 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846790871 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32124/statm): 531 226 485 147 0 384 0
[pid=32124] vsize: 2124
Raw data (/proc/32128/stat): 32128 (minisat+_64-bit) R 32124 32124 20728 0 -1 0 19700 0 0 0 120715 143 0 0 25 0 1 0 1846790876 83451904 19331 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32128/statm): 20374 19331 145 145 0 20229 0
[pid=32128] vsize: 81496
Current children cumulated CPU time (s) 1208.59
Current children cumulated vsize (Kb) 83620

Sending SIGTERM to -32124
Sleeping 2 seconds
One traced child (pid=32124) ended because it received signal 15 (SIGTERM)
One traced child (pid=32128) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.15
CPU time (s): 1208.63
CPU user time (s): 1207.15
CPU system time (s): 1.47678
CPU usage (%): 99.8741
Max. virtual memory (cumulated for all children) (Kb): 83620