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/4836/stat): 4836 (minisat+_script) R 4835 4836 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797779496 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/4836/statm): 174 3 169 147 0 27 0
[pid=4836] 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=4837
New process pid=4838
New process pid=4839
execve syscall for /bin/sed executable
One traced child (pid=4838) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=4839) exited with status: 0
One traced child (pid=4837) exited with status: 0
New process pid=4840
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-bg512142.opb

[startup+10.0041 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) T 4836 4836 31915 0 -1 0 20118 0 0 0 840 78 0 0 22 0 1 0 1797779501 85422080 18721 4294967295 134512640 135094434 3221224432 3221216972 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4840/statm): 20855 18721 145 145 0 20710 0
[pid=4840] vsize: 83420
Current children cumulated CPU time (s) 9.19
Current children cumulated vsize (Kb) 85544

[startup+20.0049 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28113 0 0 0 1773 112 0 0 25 0 1 0 1797779501 126316544 26716 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 30839 26716 145 145 0 30694 0
[pid=4840] vsize: 123356
Current children cumulated CPU time (s) 18.86
Current children cumulated vsize (Kb) 125480

[startup+30.0068 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28164 0 0 0 2771 112 0 0 25 0 1 0 1797779501 126492672 26767 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 30882 26767 145 145 0 30737 0
[pid=4840] vsize: 123528
Current children cumulated CPU time (s) 28.84
Current children cumulated vsize (Kb) 125652

[startup+40.0076 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28234 0 0 0 3771 112 0 0 25 0 1 0 1797779501 126697472 26837 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 30932 26837 145 145 0 30787 0
[pid=4840] vsize: 123728
Current children cumulated CPU time (s) 38.84
Current children cumulated vsize (Kb) 125852

[startup+50.0084 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28294 0 0 0 4770 113 0 0 25 0 1 0 1797779501 126869504 26897 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 30974 26897 145 145 0 30829 0
[pid=4840] vsize: 123896
Current children cumulated CPU time (s) 48.84
Current children cumulated vsize (Kb) 126020

[startup+60.0093 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28313 0 0 0 5770 113 0 0 25 0 1 0 1797779501 126935040 26916 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 30990 26916 145 145 0 30845 0
[pid=4840] vsize: 123960
Current children cumulated CPU time (s) 58.84
Current children cumulated vsize (Kb) 126084

[startup+70.0101 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28325 0 0 0 6770 113 0 0 25 0 1 0 1797779501 126988288 26928 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31003 26928 145 145 0 30858 0
[pid=4840] vsize: 124012
Current children cumulated CPU time (s) 68.84
Current children cumulated vsize (Kb) 126136

[startup+80.0109 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28344 0 0 0 7770 113 0 0 25 0 1 0 1797779501 127041536 26947 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31016 26947 145 145 0 30871 0
[pid=4840] vsize: 124064
Current children cumulated CPU time (s) 78.84
Current children cumulated vsize (Kb) 126188

[startup+90.0118 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28357 0 0 0 8770 113 0 0 25 0 1 0 1797779501 127086592 26960 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31027 26960 145 145 0 30882 0
[pid=4840] vsize: 124108
Current children cumulated CPU time (s) 88.84
Current children cumulated vsize (Kb) 126232

[startup+100.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28374 0 0 0 9770 114 0 0 25 0 1 0 1797779501 127139840 26977 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31040 26977 145 145 0 30895 0
[pid=4840] vsize: 124160
Current children cumulated CPU time (s) 98.85
Current children cumulated vsize (Kb) 126284

[startup+110.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28410 0 0 0 10769 114 0 0 25 0 1 0 1797779501 127217664 27013 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31059 27013 145 145 0 30914 0
[pid=4840] vsize: 124236
Current children cumulated CPU time (s) 108.84
Current children cumulated vsize (Kb) 126360

[startup+120.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28438 0 0 0 11769 114 0 0 25 0 1 0 1797779501 127283200 27041 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31075 27041 145 145 0 30930 0
[pid=4840] vsize: 124300
Current children cumulated CPU time (s) 118.84
Current children cumulated vsize (Kb) 126424

[startup+130.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28451 0 0 0 12769 114 0 0 25 0 1 0 1797779501 127336448 27054 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31088 27054 145 145 0 30943 0
[pid=4840] vsize: 124352
Current children cumulated CPU time (s) 128.84
Current children cumulated vsize (Kb) 126476

[startup+140.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28463 0 0 0 13769 114 0 0 25 0 1 0 1797779501 127393792 27066 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31102 27066 145 145 0 30957 0
[pid=4840] vsize: 124408
Current children cumulated CPU time (s) 138.84
Current children cumulated vsize (Kb) 126532

[startup+150.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28492 0 0 0 14769 114 0 0 25 0 1 0 1797779501 127459328 27095 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31118 27095 145 145 0 30973 0
[pid=4840] vsize: 124472
Current children cumulated CPU time (s) 148.84
Current children cumulated vsize (Kb) 126596

[startup+160.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28499 0 0 0 15769 115 0 0 25 0 1 0 1797779501 127488000 27102 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31125 27102 145 145 0 30980 0
[pid=4840] vsize: 124500
Current children cumulated CPU time (s) 158.85
Current children cumulated vsize (Kb) 126624

[startup+170.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28518 0 0 0 16769 115 0 0 25 0 1 0 1797779501 127533056 27121 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31136 27121 145 145 0 30991 0
[pid=4840] vsize: 124544
Current children cumulated CPU time (s) 168.85
Current children cumulated vsize (Kb) 126668

[startup+180.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28535 0 0 0 17769 115 0 0 25 0 1 0 1797779501 127590400 27138 4294967295 134512640 135094434 3221224432 3221223100 134553522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31150 27138 145 145 0 31005 0
[pid=4840] vsize: 124600
Current children cumulated CPU time (s) 178.85
Current children cumulated vsize (Kb) 126724

[startup+190.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28542 0 0 0 18769 115 0 0 25 0 1 0 1797779501 127614976 27145 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31156 27145 145 145 0 31011 0
[pid=4840] vsize: 124624
Current children cumulated CPU time (s) 188.85
Current children cumulated vsize (Kb) 126748

[startup+200.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28545 0 0 0 19769 115 0 0 25 0 1 0 1797779501 127627264 27148 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31159 27148 145 145 0 31014 0
[pid=4840] vsize: 124636
Current children cumulated CPU time (s) 198.85
Current children cumulated vsize (Kb) 126760

[startup+210.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28564 0 0 0 20770 115 0 0 25 0 1 0 1797779501 127676416 27167 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31171 27167 145 145 0 31026 0
[pid=4840] vsize: 124684
Current children cumulated CPU time (s) 208.86
Current children cumulated vsize (Kb) 126808

[startup+220.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28569 0 0 0 21769 115 0 0 25 0 1 0 1797779501 127696896 27172 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31176 27172 145 145 0 31031 0
[pid=4840] vsize: 124704
Current children cumulated CPU time (s) 218.85
Current children cumulated vsize (Kb) 126828

[startup+230.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28573 0 0 0 22770 115 0 0 25 0 1 0 1797779501 127713280 27176 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31180 27176 145 145 0 31035 0
[pid=4840] vsize: 124720
Current children cumulated CPU time (s) 228.86
Current children cumulated vsize (Kb) 126844

[startup+240.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28578 0 0 0 23770 115 0 0 25 0 1 0 1797779501 127733760 27181 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31185 27181 145 145 0 31040 0
[pid=4840] vsize: 124740
Current children cumulated CPU time (s) 238.86
Current children cumulated vsize (Kb) 126864

[startup+250.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28605 0 0 0 24770 115 0 0 25 0 1 0 1797779501 127848448 27208 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31213 27208 145 145 0 31068 0
[pid=4840] vsize: 124852
Current children cumulated CPU time (s) 248.86
Current children cumulated vsize (Kb) 126976

[startup+260.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28615 0 0 0 25770 115 0 0 25 0 1 0 1797779501 127868928 27218 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31218 27218 145 145 0 31073 0
[pid=4840] vsize: 124872
Current children cumulated CPU time (s) 258.86
Current children cumulated vsize (Kb) 126996

[startup+270.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28633 0 0 0 26770 116 0 0 25 0 1 0 1797779501 127909888 27236 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31228 27236 145 145 0 31083 0
[pid=4840] vsize: 124912
Current children cumulated CPU time (s) 268.87
Current children cumulated vsize (Kb) 127036

[startup+280.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28649 0 0 0 27770 116 0 0 25 0 1 0 1797779501 127946752 27252 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31237 27252 145 145 0 31092 0
[pid=4840] vsize: 124948
Current children cumulated CPU time (s) 278.87
Current children cumulated vsize (Kb) 127072

[startup+290.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28656 0 0 0 28770 116 0 0 25 0 1 0 1797779501 127971328 27259 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31243 27259 145 145 0 31098 0
[pid=4840] vsize: 124972
Current children cumulated CPU time (s) 288.87
Current children cumulated vsize (Kb) 127096

[startup+300.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28662 0 0 0 29770 116 0 0 25 0 1 0 1797779501 127995904 27265 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31249 27265 145 145 0 31104 0
[pid=4840] vsize: 124996
Current children cumulated CPU time (s) 298.87
Current children cumulated vsize (Kb) 127120

[startup+310.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28665 0 0 0 30770 116 0 0 25 0 1 0 1797779501 128004096 27268 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31251 27268 145 145 0 31106 0
[pid=4840] vsize: 125004
Current children cumulated CPU time (s) 308.87
Current children cumulated vsize (Kb) 127128

[startup+320.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28670 0 0 0 31770 116 0 0 25 0 1 0 1797779501 128024576 27273 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31256 27273 145 145 0 31111 0
[pid=4840] vsize: 125024
Current children cumulated CPU time (s) 318.87
Current children cumulated vsize (Kb) 127148

[startup+330.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28687 0 0 0 32770 116 0 0 25 0 1 0 1797779501 128061440 27290 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31265 27290 145 145 0 31120 0
[pid=4840] vsize: 125060
Current children cumulated CPU time (s) 328.87
Current children cumulated vsize (Kb) 127184

[startup+340.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28694 0 0 0 33770 116 0 0 25 0 1 0 1797779501 128090112 27297 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31272 27297 145 145 0 31127 0
[pid=4840] vsize: 125088
Current children cumulated CPU time (s) 338.87
Current children cumulated vsize (Kb) 127212

[startup+350.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28703 0 0 0 34771 116 0 0 25 0 1 0 1797779501 128122880 27306 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31280 27306 145 145 0 31135 0
[pid=4840] vsize: 125120
Current children cumulated CPU time (s) 348.88
Current children cumulated vsize (Kb) 127244

[startup+360.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28708 0 0 0 35771 116 0 0 25 0 1 0 1797779501 128143360 27311 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31285 27311 145 145 0 31140 0
[pid=4840] vsize: 125140
Current children cumulated CPU time (s) 358.88
Current children cumulated vsize (Kb) 127264

[startup+370.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28714 0 0 0 36771 116 0 0 25 0 1 0 1797779501 128167936 27317 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31291 27317 145 145 0 31146 0
[pid=4840] vsize: 125164
Current children cumulated CPU time (s) 368.88
Current children cumulated vsize (Kb) 127288

[startup+380.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28739 0 0 0 37771 117 0 0 25 0 1 0 1797779501 128225280 27342 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31305 27342 145 145 0 31160 0
[pid=4840] vsize: 125220
Current children cumulated CPU time (s) 378.89
Current children cumulated vsize (Kb) 127344

[startup+390.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28750 0 0 0 38771 117 0 0 25 0 1 0 1797779501 128270336 27353 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31316 27353 145 145 0 31171 0
[pid=4840] vsize: 125264
Current children cumulated CPU time (s) 388.89
Current children cumulated vsize (Kb) 127388

[startup+400.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28754 0 0 0 39771 117 0 0 25 0 1 0 1797779501 128282624 27357 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31319 27357 145 145 0 31174 0
[pid=4840] vsize: 125276
Current children cumulated CPU time (s) 398.89
Current children cumulated vsize (Kb) 127400

[startup+410.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28762 0 0 0 40771 117 0 0 25 0 1 0 1797779501 128315392 27365 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31327 27365 145 145 0 31182 0
[pid=4840] vsize: 125308
Current children cumulated CPU time (s) 408.89
Current children cumulated vsize (Kb) 127432

[startup+420.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28768 0 0 0 41771 117 0 0 25 0 1 0 1797779501 128339968 27371 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31333 27371 145 145 0 31188 0
[pid=4840] vsize: 125332
Current children cumulated CPU time (s) 418.89
Current children cumulated vsize (Kb) 127456

[startup+430.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28790 0 0 0 42771 117 0 0 25 0 1 0 1797779501 128491520 27393 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31370 27393 145 145 0 31225 0
[pid=4840] vsize: 125480
Current children cumulated CPU time (s) 428.89
Current children cumulated vsize (Kb) 127604

[startup+440.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28790 0 0 0 43772 117 0 0 25 0 1 0 1797779501 128491520 27393 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31370 27393 145 145 0 31225 0
[pid=4840] vsize: 125480
Current children cumulated CPU time (s) 438.9
Current children cumulated vsize (Kb) 127604

[startup+450.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28791 0 0 0 44772 117 0 0 25 0 1 0 1797779501 128491520 27394 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31370 27394 145 145 0 31225 0
[pid=4840] vsize: 125480
Current children cumulated CPU time (s) 448.9
Current children cumulated vsize (Kb) 127604

[startup+460.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28792 0 0 0 45772 117 0 0 25 0 1 0 1797779501 128495616 27395 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31371 27395 145 145 0 31226 0
[pid=4840] vsize: 125484
Current children cumulated CPU time (s) 458.9
Current children cumulated vsize (Kb) 127608

[startup+470.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28804 0 0 0 46772 117 0 0 25 0 1 0 1797779501 128532480 27407 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31380 27407 145 145 0 31235 0
[pid=4840] vsize: 125520
Current children cumulated CPU time (s) 468.9
Current children cumulated vsize (Kb) 127644

[startup+480.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28812 0 0 0 47773 117 0 0 25 0 1 0 1797779501 128565248 27415 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31388 27415 145 145 0 31243 0
[pid=4840] vsize: 125552
Current children cumulated CPU time (s) 478.91
Current children cumulated vsize (Kb) 127676

[startup+490.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28837 0 0 0 48773 117 0 0 25 0 1 0 1797779501 128614400 27440 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31400 27440 145 145 0 31255 0
[pid=4840] vsize: 125600
Current children cumulated CPU time (s) 488.91
Current children cumulated vsize (Kb) 127724

[startup+500.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28844 0 0 0 49773 117 0 0 25 0 1 0 1797779501 128643072 27447 4294967295 134512640 135094434 3221224432 3221223072 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31407 27447 145 145 0 31262 0
[pid=4840] vsize: 125628
Current children cumulated CPU time (s) 498.91
Current children cumulated vsize (Kb) 127752

[startup+510.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28855 0 0 0 50773 117 0 0 25 0 1 0 1797779501 128684032 27458 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31417 27458 145 145 0 31272 0
[pid=4840] vsize: 125668
Current children cumulated CPU time (s) 508.91
Current children cumulated vsize (Kb) 127792

[startup+520.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28857 0 0 0 51773 117 0 0 25 0 1 0 1797779501 128692224 27460 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31419 27460 145 145 0 31274 0
[pid=4840] vsize: 125676
Current children cumulated CPU time (s) 518.91
Current children cumulated vsize (Kb) 127800

[startup+530.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28871 0 0 0 52773 117 0 0 25 0 1 0 1797779501 128724992 27474 4294967295 134512640 135094434 3221224432 3221223044 134563030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31427 27474 145 145 0 31282 0
[pid=4840] vsize: 125708
Current children cumulated CPU time (s) 528.91
Current children cumulated vsize (Kb) 127832

[startup+540.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28885 0 0 0 53773 117 0 0 25 0 1 0 1797779501 128765952 27488 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31437 27488 145 145 0 31292 0
[pid=4840] vsize: 125748
Current children cumulated CPU time (s) 538.91
Current children cumulated vsize (Kb) 127872

[startup+550.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28888 0 0 0 54773 117 0 0 25 0 1 0 1797779501 128778240 27491 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31440 27491 145 145 0 31295 0
[pid=4840] vsize: 125760
Current children cumulated CPU time (s) 548.91
Current children cumulated vsize (Kb) 127884

[startup+560.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28892 0 0 0 55774 118 0 0 25 0 1 0 1797779501 128790528 27495 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31443 27495 145 145 0 31298 0
[pid=4840] vsize: 125772
Current children cumulated CPU time (s) 558.93
Current children cumulated vsize (Kb) 127896

[startup+570.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28895 0 0 0 56774 118 0 0 25 0 1 0 1797779501 128802816 27498 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31446 27498 145 145 0 31301 0
[pid=4840] vsize: 125784
Current children cumulated CPU time (s) 568.93
Current children cumulated vsize (Kb) 127908

[startup+580.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28899 0 0 0 57772 119 0 0 25 0 1 0 1797779501 128819200 27502 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4840/statm): 31450 27502 145 145 0 31305 0
[pid=4840] vsize: 125800
Current children cumulated CPU time (s) 578.92
Current children cumulated vsize (Kb) 127924

[startup+590.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28922 0 0 0 58771 120 0 0 25 0 1 0 1797779501 128864256 27525 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31461 27525 145 145 0 31316 0
[pid=4840] vsize: 125844
Current children cumulated CPU time (s) 588.92
Current children cumulated vsize (Kb) 127968

[startup+600.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28924 0 0 0 59771 120 0 0 25 0 1 0 1797779501 128872448 27527 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31463 27527 145 145 0 31318 0
[pid=4840] vsize: 125852
Current children cumulated CPU time (s) 598.92
Current children cumulated vsize (Kb) 127976

[startup+610.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28926 0 0 0 60771 120 0 0 25 0 1 0 1797779501 128880640 27529 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31465 27529 145 145 0 31320 0
[pid=4840] vsize: 125860
Current children cumulated CPU time (s) 608.92
Current children cumulated vsize (Kb) 127984

[startup+620.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28936 0 0 0 61771 120 0 0 25 0 1 0 1797779501 128917504 27539 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31474 27539 145 145 0 31329 0
[pid=4840] vsize: 125896
Current children cumulated CPU time (s) 618.92
Current children cumulated vsize (Kb) 128020

[startup+630.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 28948 0 0 0 62771 120 0 0 25 0 1 0 1797779501 128962560 27551 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31485 27551 145 145 0 31340 0
[pid=4840] vsize: 125940
Current children cumulated CPU time (s) 628.92
Current children cumulated vsize (Kb) 128064

[startup+640.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29045 0 0 0 63771 120 0 0 25 0 1 0 1797779501 129343488 27648 4294967295 134512640 135094434 3221224432 3221223044 134563085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31578 27648 145 145 0 31433 0
[pid=4840] vsize: 126312
Current children cumulated CPU time (s) 638.92
Current children cumulated vsize (Kb) 128436

[startup+650.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29067 0 0 0 64770 120 0 0 25 0 1 0 1797779501 129429504 27670 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31599 27670 145 145 0 31454 0
[pid=4840] vsize: 126396
Current children cumulated CPU time (s) 648.91
Current children cumulated vsize (Kb) 128520

[startup+660.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29071 0 0 0 65771 121 0 0 25 0 1 0 1797779501 129445888 27674 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31603 27674 145 145 0 31458 0
[pid=4840] vsize: 126412
Current children cumulated CPU time (s) 658.93
Current children cumulated vsize (Kb) 128536

[startup+670.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29076 0 0 0 66771 121 0 0 25 0 1 0 1797779501 129466368 27679 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31608 27679 145 145 0 31463 0
[pid=4840] vsize: 126432
Current children cumulated CPU time (s) 668.93
Current children cumulated vsize (Kb) 128556

[startup+680.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29082 0 0 0 67771 121 0 0 25 0 1 0 1797779501 129486848 27685 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31613 27685 145 145 0 31468 0
[pid=4840] vsize: 126452
Current children cumulated CPU time (s) 678.93
Current children cumulated vsize (Kb) 128576

[startup+690.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29087 0 0 0 68771 121 0 0 25 0 1 0 1797779501 129507328 27690 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31618 27690 145 145 0 31473 0
[pid=4840] vsize: 126472
Current children cumulated CPU time (s) 688.93
Current children cumulated vsize (Kb) 128596

[startup+700.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29126 0 0 0 69771 121 0 0 25 0 1 0 1797779501 129794048 27729 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31688 27729 145 145 0 31543 0
[pid=4840] vsize: 126752
Current children cumulated CPU time (s) 698.93
Current children cumulated vsize (Kb) 128876

[startup+710.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29126 0 0 0 70771 121 0 0 25 0 1 0 1797779501 129794048 27729 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31688 27729 145 145 0 31543 0
[pid=4840] vsize: 126752
Current children cumulated CPU time (s) 708.93
Current children cumulated vsize (Kb) 128876

[startup+720.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29127 0 0 0 71771 121 0 0 25 0 1 0 1797779501 129794048 27730 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31688 27730 145 145 0 31543 0
[pid=4840] vsize: 126752
Current children cumulated CPU time (s) 718.93
Current children cumulated vsize (Kb) 128876

[startup+730.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29136 0 0 0 72771 121 0 0 25 0 1 0 1797779501 129826816 27739 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31696 27739 145 145 0 31551 0
[pid=4840] vsize: 126784
Current children cumulated CPU time (s) 728.93
Current children cumulated vsize (Kb) 128908

[startup+740.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29157 0 0 0 73771 121 0 0 25 0 1 0 1797779501 129908736 27760 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31716 27760 145 145 0 31571 0
[pid=4840] vsize: 126864
Current children cumulated CPU time (s) 738.93
Current children cumulated vsize (Kb) 128988

[startup+750.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29172 0 0 0 74771 121 0 0 25 0 1 0 1797779501 129966080 27775 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31730 27775 145 145 0 31585 0
[pid=4840] vsize: 126920
Current children cumulated CPU time (s) 748.93
Current children cumulated vsize (Kb) 129044

[startup+760.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29183 0 0 0 75771 121 0 0 25 0 1 0 1797779501 130007040 27786 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31740 27786 145 145 0 31595 0
[pid=4840] vsize: 126960
Current children cumulated CPU time (s) 758.93
Current children cumulated vsize (Kb) 129084

[startup+770.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29201 0 0 0 76771 121 0 0 25 0 1 0 1797779501 130076672 27804 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31757 27804 145 145 0 31612 0
[pid=4840] vsize: 127028
Current children cumulated CPU time (s) 768.93
Current children cumulated vsize (Kb) 129152

[startup+780.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29210 0 0 0 77771 121 0 0 25 0 1 0 1797779501 130113536 27813 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31766 27813 145 145 0 31621 0
[pid=4840] vsize: 127064
Current children cumulated CPU time (s) 778.93
Current children cumulated vsize (Kb) 129188

[startup+790.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29216 0 0 0 78771 121 0 0 25 0 1 0 1797779501 130134016 27819 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31771 27819 145 145 0 31626 0
[pid=4840] vsize: 127084
Current children cumulated CPU time (s) 788.93
Current children cumulated vsize (Kb) 129208

[startup+800.068 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29228 0 0 0 79771 121 0 0 25 0 1 0 1797779501 130183168 27831 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31783 27831 145 145 0 31638 0
[pid=4840] vsize: 127132
Current children cumulated CPU time (s) 798.93
Current children cumulated vsize (Kb) 129256

[startup+810.069 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29241 0 0 0 80771 121 0 0 25 0 1 0 1797779501 130232320 27844 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31795 27844 145 145 0 31650 0
[pid=4840] vsize: 127180
Current children cumulated CPU time (s) 808.93
Current children cumulated vsize (Kb) 129304

[startup+820.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29254 0 0 0 81771 122 0 0 25 0 1 0 1797779501 130281472 27857 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31807 27857 145 145 0 31662 0
[pid=4840] vsize: 127228
Current children cumulated CPU time (s) 818.94
Current children cumulated vsize (Kb) 129352

[startup+830.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29264 0 0 0 82771 122 0 0 25 0 1 0 1797779501 130318336 27867 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31816 27867 145 145 0 31671 0
[pid=4840] vsize: 127264
Current children cumulated CPU time (s) 828.94
Current children cumulated vsize (Kb) 129388

[startup+840.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29271 0 0 0 83771 122 0 0 25 0 1 0 1797779501 130347008 27874 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31823 27874 145 145 0 31678 0
[pid=4840] vsize: 127292
Current children cumulated CPU time (s) 838.94
Current children cumulated vsize (Kb) 129416

[startup+850.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29283 0 0 0 84771 122 0 0 25 0 1 0 1797779501 130392064 27886 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31834 27886 145 145 0 31689 0
[pid=4840] vsize: 127336
Current children cumulated CPU time (s) 848.94
Current children cumulated vsize (Kb) 129460

[startup+860.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29307 0 0 0 85771 122 0 0 25 0 1 0 1797779501 130486272 27910 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31857 27910 145 145 0 31712 0
[pid=4840] vsize: 127428
Current children cumulated CPU time (s) 858.94
Current children cumulated vsize (Kb) 129552

[startup+870.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29319 0 0 0 86772 122 0 0 25 0 1 0 1797779501 130531328 27922 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31868 27922 145 145 0 31723 0
[pid=4840] vsize: 127472
Current children cumulated CPU time (s) 868.95
Current children cumulated vsize (Kb) 129596

[startup+880.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29332 0 0 0 87772 122 0 0 25 0 1 0 1797779501 130580480 27935 4294967295 134512640 135094434 3221224432 3221223136 134559010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31880 27935 145 145 0 31735 0
[pid=4840] vsize: 127520
Current children cumulated CPU time (s) 878.95
Current children cumulated vsize (Kb) 129644

[startup+890.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29335 0 0 0 88772 122 0 0 25 0 1 0 1797779501 130592768 27938 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31883 27938 145 145 0 31738 0
[pid=4840] vsize: 127532
Current children cumulated CPU time (s) 888.95
Current children cumulated vsize (Kb) 129656

[startup+900.076 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29346 0 0 0 89772 122 0 0 25 0 1 0 1797779501 130633728 27949 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31893 27949 145 145 0 31748 0
[pid=4840] vsize: 127572
Current children cumulated CPU time (s) 898.95
Current children cumulated vsize (Kb) 129696

[startup+910.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29358 0 0 0 90772 122 0 0 25 0 1 0 1797779501 130682880 27961 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31905 27961 145 145 0 31760 0
[pid=4840] vsize: 127620
Current children cumulated CPU time (s) 908.95
Current children cumulated vsize (Kb) 129744

[startup+920.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29377 0 0 0 91772 122 0 0 25 0 1 0 1797779501 130756608 27980 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31923 27980 145 145 0 31778 0
[pid=4840] vsize: 127692
Current children cumulated CPU time (s) 918.95
Current children cumulated vsize (Kb) 129816

[startup+930.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29390 0 0 0 92772 122 0 0 25 0 1 0 1797779501 130805760 27993 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31935 27993 145 145 0 31790 0
[pid=4840] vsize: 127740
Current children cumulated CPU time (s) 928.95
Current children cumulated vsize (Kb) 129864

[startup+940.078 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29398 0 0 0 93772 123 0 0 25 0 1 0 1797779501 130834432 28001 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31942 28001 145 145 0 31797 0
[pid=4840] vsize: 127768
Current children cumulated CPU time (s) 938.96
Current children cumulated vsize (Kb) 129892

[startup+950.079 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29405 0 0 0 94772 123 0 0 25 0 1 0 1797779501 130863104 28008 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31949 28008 145 145 0 31804 0
[pid=4840] vsize: 127796
Current children cumulated CPU time (s) 948.96
Current children cumulated vsize (Kb) 129920

[startup+960.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29412 0 0 0 95772 123 0 0 25 0 1 0 1797779501 130887680 28015 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31955 28015 145 145 0 31810 0
[pid=4840] vsize: 127820
Current children cumulated CPU time (s) 958.96
Current children cumulated vsize (Kb) 129944

[startup+970.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29421 0 0 0 96772 123 0 0 25 0 1 0 1797779501 130924544 28024 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31964 28024 145 145 0 31819 0
[pid=4840] vsize: 127856
Current children cumulated CPU time (s) 968.96
Current children cumulated vsize (Kb) 129980

[startup+980.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29431 0 0 0 97772 123 0 0 25 0 1 0 1797779501 130961408 28034 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31973 28034 145 145 0 31828 0
[pid=4840] vsize: 127892
Current children cumulated CPU time (s) 978.96
Current children cumulated vsize (Kb) 130016

[startup+990.082 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29456 0 0 0 98771 124 0 0 25 0 1 0 1797779501 131059712 28059 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 31997 28059 145 145 0 31852 0
[pid=4840] vsize: 127988
Current children cumulated CPU time (s) 988.96
Current children cumulated vsize (Kb) 130112

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29474 0 0 0 99771 124 0 0 25 0 1 0 1797779501 131129344 28077 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32014 28077 145 145 0 31869 0
[pid=4840] vsize: 128056
Current children cumulated CPU time (s) 998.96
Current children cumulated vsize (Kb) 130180

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29495 0 0 0 100771 124 0 0 25 0 1 0 1797779501 131211264 28098 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32034 28098 145 145 0 31889 0
[pid=4840] vsize: 128136
Current children cumulated CPU time (s) 1008.96
Current children cumulated vsize (Kb) 130260

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29504 0 0 0 101771 124 0 0 25 0 1 0 1797779501 131244032 28107 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32042 28107 145 145 0 31897 0
[pid=4840] vsize: 128168
Current children cumulated CPU time (s) 1018.96
Current children cumulated vsize (Kb) 130292

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29518 0 0 0 102771 124 0 0 25 0 1 0 1797779501 131297280 28121 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32055 28121 145 145 0 31910 0
[pid=4840] vsize: 128220
Current children cumulated CPU time (s) 1028.96
Current children cumulated vsize (Kb) 130344

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29528 0 0 0 103771 124 0 0 25 0 1 0 1797779501 131334144 28131 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32064 28131 145 145 0 31919 0
[pid=4840] vsize: 128256
Current children cumulated CPU time (s) 1038.96
Current children cumulated vsize (Kb) 130380

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29540 0 0 0 104771 124 0 0 25 0 1 0 1797779501 131383296 28143 4294967295 134512640 135094434 3221224432 3221223044 134563039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32076 28143 145 145 0 31931 0
[pid=4840] vsize: 128304
Current children cumulated CPU time (s) 1048.96
Current children cumulated vsize (Kb) 130428

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29552 0 0 0 105771 124 0 0 25 0 1 0 1797779501 131428352 28155 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32087 28155 145 145 0 31942 0
[pid=4840] vsize: 128348
Current children cumulated CPU time (s) 1058.96
Current children cumulated vsize (Kb) 130472

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29756 0 0 0 106767 126 0 0 25 0 1 0 1797779501 132218880 28359 4294967295 134512640 135094434 3221224432 3221223104 134555846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32280 28359 145 145 0 32135 0
[pid=4840] vsize: 129120
Current children cumulated CPU time (s) 1068.94
Current children cumulated vsize (Kb) 131244

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29783 0 0 0 107767 126 0 0 25 0 1 0 1797779501 132325376 28386 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32306 28386 145 145 0 32161 0
[pid=4840] vsize: 129224
Current children cumulated CPU time (s) 1078.94
Current children cumulated vsize (Kb) 131348

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29800 0 0 0 108766 126 0 0 25 0 1 0 1797779501 132653056 28403 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32386 28403 145 145 0 32241 0
[pid=4840] vsize: 129544
Current children cumulated CPU time (s) 1088.93
Current children cumulated vsize (Kb) 131668

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29812 0 0 0 109767 126 0 0 25 0 1 0 1797779501 132698112 28415 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32397 28415 145 145 0 32252 0
[pid=4840] vsize: 129588
Current children cumulated CPU time (s) 1098.94
Current children cumulated vsize (Kb) 131712

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29857 0 0 0 110765 126 0 0 25 0 1 0 1797779501 132878336 28460 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32441 28460 145 145 0 32296 0
[pid=4840] vsize: 129764
Current children cumulated CPU time (s) 1108.92
Current children cumulated vsize (Kb) 131888

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29883 0 0 0 111765 127 0 0 25 0 1 0 1797779501 132980736 28486 4294967295 134512640 135094434 3221224432 3221223056 134557633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32466 28486 145 145 0 32321 0
[pid=4840] vsize: 129864
Current children cumulated CPU time (s) 1118.93
Current children cumulated vsize (Kb) 131988

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29908 0 0 0 112765 127 0 0 25 0 1 0 1797779501 133079040 28511 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32490 28511 145 145 0 32345 0
[pid=4840] vsize: 129960
Current children cumulated CPU time (s) 1128.93
Current children cumulated vsize (Kb) 132084

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29918 0 0 0 113765 127 0 0 25 0 1 0 1797779501 133115904 28521 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32499 28521 145 145 0 32354 0
[pid=4840] vsize: 129996
Current children cumulated CPU time (s) 1138.93
Current children cumulated vsize (Kb) 132120

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29939 0 0 0 114765 127 0 0 25 0 1 0 1797779501 133197824 28542 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32519 28542 145 145 0 32374 0
[pid=4840] vsize: 130076
Current children cumulated CPU time (s) 1148.93
Current children cumulated vsize (Kb) 132200

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29960 0 0 0 115765 127 0 0 25 0 1 0 1797779501 133271552 28563 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32537 28563 145 145 0 32392 0
[pid=4840] vsize: 130148
Current children cumulated CPU time (s) 1158.93
Current children cumulated vsize (Kb) 132272

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 29990 0 0 0 116764 128 0 0 25 0 1 0 1797779501 133390336 28593 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32566 28593 145 145 0 32421 0
[pid=4840] vsize: 130264
Current children cumulated CPU time (s) 1168.93
Current children cumulated vsize (Kb) 132388

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 30068 0 0 0 117763 128 0 0 25 0 1 0 1797779501 133697536 28671 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32641 28671 145 145 0 32496 0
[pid=4840] vsize: 130564
Current children cumulated CPU time (s) 1178.92
Current children cumulated vsize (Kb) 132688

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 30080 0 0 0 118763 128 0 0 25 0 1 0 1797779501 133746688 28683 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32653 28683 145 145 0 32508 0
[pid=4840] vsize: 130612
Current children cumulated CPU time (s) 1188.92
Current children cumulated vsize (Kb) 132736

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 30097 0 0 0 119763 129 0 0 25 0 1 0 1797779501 133812224 28700 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32669 28700 145 145 0 32524 0
[pid=4840] vsize: 130676
Current children cumulated CPU time (s) 1198.93
Current children cumulated vsize (Kb) 132800

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 30120 0 0 0 120763 129 0 0 25 0 1 0 1797779501 133898240 28723 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32690 28723 145 145 0 32545 0
[pid=4840] vsize: 130760
Current children cumulated CPU time (s) 1208.93
Current children cumulated vsize (Kb) 132884



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4840
Raw data (/proc/4836/stat): 4836 (minisat+_script) S 4835 4836 31915 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797779496 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4836/statm): 531 226 485 147 0 384 0
[pid=4836] vsize: 2124
Raw data (/proc/4840/stat): 4840 (minisat+_64-bit) R 4836 4836 31915 0 -1 0 30120 0 0 0 120763 129 0 0 25 0 1 0 1797779501 133898240 28723 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4840/statm): 32690 28723 145 145 0 32545 0
[pid=4840] vsize: 130760
Current children cumulated CPU time (s) 1208.93
Current children cumulated vsize (Kb) 132884

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.98
CPU user time (s): 1207.63
CPU system time (s): 1.35179
CPU usage (%): 99.903
Max. virtual memory (cumulated for all children) (Kb): 132884