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

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.95 0.89 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8431 0 0 0 924 35 0 0 25 0 1 0 1793723053 36999168 8104 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 9033 8104 145 145 0 8888 0
[pid=13373] vsize: 36132
Current children cumulated CPU time (s) 9.61
Current children cumulated vsize (Kb) 38256

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.96 0.89 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8448 0 0 0 1924 35 0 0 25 0 1 0 1793723053 37048320 8121 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9045 8121 145 145 0 8900 0
[pid=13373] vsize: 36180
Current children cumulated CPU time (s) 19.61
Current children cumulated vsize (Kb) 38304

[startup+30.0061 s]
Raw data (loadavg): 0.95 0.96 0.89 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8479 0 0 0 2922 36 0 0 25 0 1 0 1793723053 37146624 8152 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9069 8152 145 145 0 8924 0
[pid=13373] vsize: 36276
Current children cumulated CPU time (s) 29.6
Current children cumulated vsize (Kb) 38400

[startup+40.0068 s]
Raw data (loadavg): 0.95 0.96 0.89 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8507 0 0 0 3922 36 0 0 25 0 1 0 1793723053 37236736 8180 4294967295 134512640 135094434 3221224432 3221223088 134557774 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9091 8180 145 145 0 8946 0
[pid=13373] vsize: 36364
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 38488

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.96 0.89 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8541 0 0 0 4922 36 0 0 25 0 1 0 1793723053 37380096 8214 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9126 8214 145 145 0 8981 0
[pid=13373] vsize: 36504
Current children cumulated CPU time (s) 49.6
Current children cumulated vsize (Kb) 38628

[startup+60.0072 s]
Raw data (loadavg): 0.97 0.96 0.89 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8575 0 0 0 5922 37 0 0 25 0 1 0 1793723053 37494784 8248 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9154 8248 145 145 0 9009 0
[pid=13373] vsize: 36616
Current children cumulated CPU time (s) 59.61
Current children cumulated vsize (Kb) 38740

[startup+70.0079 s]
Raw data (loadavg): 0.97 0.96 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8598 0 0 0 6922 37 0 0 25 0 1 0 1793723053 37560320 8271 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9170 8271 145 145 0 9025 0
[pid=13373] vsize: 36680
Current children cumulated CPU time (s) 69.61
Current children cumulated vsize (Kb) 38804

[startup+80.0085 s]
Raw data (loadavg): 0.98 0.96 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8637 0 0 0 7922 37 0 0 25 0 1 0 1793723053 37756928 8310 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9218 8310 145 145 0 9073 0
[pid=13373] vsize: 36872
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 38996

[startup+90.0092 s]
Raw data (loadavg): 0.98 0.96 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8667 0 0 0 8921 37 0 0 25 0 1 0 1793723053 37867520 8340 4294967295 134512640 135094434 3221224432 3221223088 134557843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9245 8340 145 145 0 9100 0
[pid=13373] vsize: 36980
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 39104

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8703 0 0 0 9921 38 0 0 25 0 1 0 1793723053 38002688 8376 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9278 8376 145 145 0 9133 0
[pid=13373] vsize: 37112
Current children cumulated CPU time (s) 99.61
Current children cumulated vsize (Kb) 39236

[startup+110.011 s]
Raw data (loadavg): 0.98 0.96 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8730 0 0 0 10920 39 0 0 25 0 1 0 1793723053 38092800 8403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 9300 8403 145 145 0 9155 0
[pid=13373] vsize: 37200
Current children cumulated CPU time (s) 109.61
Current children cumulated vsize (Kb) 39324

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8774 0 0 0 11919 39 0 0 25 0 1 0 1793723053 38260736 8447 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9341 8447 145 145 0 9196 0
[pid=13373] vsize: 37364
Current children cumulated CPU time (s) 119.6
Current children cumulated vsize (Kb) 39488

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8802 0 0 0 12919 39 0 0 25 0 1 0 1793723053 38363136 8475 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9366 8475 145 145 0 9221 0
[pid=13373] vsize: 37464
Current children cumulated CPU time (s) 129.6
Current children cumulated vsize (Kb) 39588

[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8852 0 0 0 13919 40 0 0 25 0 1 0 1793723053 38690816 8525 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9446 8525 145 145 0 9301 0
[pid=13373] vsize: 37784
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 39908

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8858 0 0 0 14919 40 0 0 25 0 1 0 1793723053 38707200 8531 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9450 8531 145 145 0 9305 0
[pid=13373] vsize: 37800
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 39924

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8887 0 0 0 15918 40 0 0 25 0 1 0 1793723053 38817792 8560 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9477 8560 145 145 0 9332 0
[pid=13373] vsize: 37908
Current children cumulated CPU time (s) 159.6
Current children cumulated vsize (Kb) 40032

[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 8923 0 0 0 16918 40 0 0 25 0 1 0 1793723053 38952960 8596 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9510 8596 145 145 0 9365 0
[pid=13373] vsize: 38040
Current children cumulated CPU time (s) 169.6
Current children cumulated vsize (Kb) 40164

[startup+180.014 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 9103 0 0 0 17915 42 0 0 25 0 1 0 1793723053 39661568 8776 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9683 8776 145 145 0 9538 0
[pid=13373] vsize: 38732
Current children cumulated CPU time (s) 179.59
Current children cumulated vsize (Kb) 40856

[startup+190.015 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 9392 0 0 0 18910 44 0 0 25 0 1 0 1793723053 40808448 9065 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 9963 9065 145 145 0 9818 0
[pid=13373] vsize: 39852
Current children cumulated CPU time (s) 189.56
Current children cumulated vsize (Kb) 41976

[startup+200.016 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 9445 0 0 0 19909 44 0 0 25 0 1 0 1793723053 41017344 9118 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 10014 9118 145 145 0 9869 0
[pid=13373] vsize: 40056
Current children cumulated CPU time (s) 199.55
Current children cumulated vsize (Kb) 42180

[startup+210.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 9849 0 0 0 20902 47 0 0 25 0 1 0 1793723053 42889216 9522 4294967295 134512640 135094434 3221224432 3221223044 134563104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 10471 9522 145 145 0 10326 0
[pid=13373] vsize: 41884
Current children cumulated CPU time (s) 209.51
Current children cumulated vsize (Kb) 44008

[startup+220.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10106 0 0 0 21898 49 0 0 25 0 1 0 1793723053 43909120 9779 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 10720 9779 145 145 0 10575 0
[pid=13373] vsize: 42880
Current children cumulated CPU time (s) 219.49
Current children cumulated vsize (Kb) 45004

[startup+230.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10272 0 0 0 22895 50 0 0 25 0 1 0 1793723053 44568576 9945 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 10881 9945 145 145 0 10736 0
[pid=13373] vsize: 43524
Current children cumulated CPU time (s) 229.47
Current children cumulated vsize (Kb) 45648

[startup+240.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10391 0 0 0 23891 52 0 0 25 0 1 0 1793723053 45039616 10064 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 10996 10064 145 145 0 10851 0
[pid=13373] vsize: 43984
Current children cumulated CPU time (s) 239.45
Current children cumulated vsize (Kb) 46108

[startup+250.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10484 0 0 0 24890 53 0 0 25 0 1 0 1793723053 45404160 10157 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 11085 10157 145 145 0 10940 0
[pid=13373] vsize: 44340
Current children cumulated CPU time (s) 249.45
Current children cumulated vsize (Kb) 46464

[startup+260.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10723 0 0 0 25887 54 0 0 25 0 1 0 1793723053 46387200 10396 4294967295 134512640 135094434 3221224432 3221223088 134561698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 11325 10396 145 145 0 11180 0
[pid=13373] vsize: 45300
Current children cumulated CPU time (s) 259.43
Current children cumulated vsize (Kb) 47424

[startup+270.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10755 0 0 0 26886 54 0 0 25 0 1 0 1793723053 46514176 10428 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 11356 10428 145 145 0 11211 0
[pid=13373] vsize: 45424
Current children cumulated CPU time (s) 269.42
Current children cumulated vsize (Kb) 47548

[startup+280.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10800 0 0 0 27886 54 0 0 25 0 1 0 1793723053 46682112 10473 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 11397 10473 145 145 0 11252 0
[pid=13373] vsize: 45588
Current children cumulated CPU time (s) 279.42
Current children cumulated vsize (Kb) 47712

[startup+290.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10834 0 0 0 28886 55 0 0 25 0 1 0 1793723053 46804992 10507 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 11427 10507 145 145 0 11282 0
[pid=13373] vsize: 45708
Current children cumulated CPU time (s) 289.43
Current children cumulated vsize (Kb) 47832

[startup+300.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10900 0 0 0 29884 55 0 0 25 0 1 0 1793723053 47063040 10573 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 11490 10573 145 145 0 11345 0
[pid=13373] vsize: 45960
Current children cumulated CPU time (s) 299.41
Current children cumulated vsize (Kb) 48084

[startup+310.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 10929 0 0 0 30883 56 0 0 25 0 1 0 1793723053 47161344 10602 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 11514 10602 145 145 0 11369 0
[pid=13373] vsize: 46056
Current children cumulated CPU time (s) 309.41
Current children cumulated vsize (Kb) 48180

[startup+320.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11007 0 0 0 31881 57 0 0 25 0 1 0 1793723053 47468544 10680 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 11589 10680 145 145 0 11444 0
[pid=13373] vsize: 46356
Current children cumulated CPU time (s) 319.4
Current children cumulated vsize (Kb) 48480

[startup+330.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11143 0 0 0 32878 59 0 0 25 0 1 0 1793723053 47996928 10816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 11718 10816 145 145 0 11573 0
[pid=13373] vsize: 46872
Current children cumulated CPU time (s) 329.39
Current children cumulated vsize (Kb) 48996

[startup+340.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11273 0 0 0 33875 60 0 0 25 0 1 0 1793723053 48513024 10946 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 11844 10946 145 145 0 11699 0
[pid=13373] vsize: 47376
Current children cumulated CPU time (s) 339.37
Current children cumulated vsize (Kb) 49500

[startup+350.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11312 0 0 0 34874 61 0 0 25 0 1 0 1793723053 48660480 10985 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 11880 10985 145 145 0 11735 0
[pid=13373] vsize: 47520
Current children cumulated CPU time (s) 349.37
Current children cumulated vsize (Kb) 49644

[startup+360.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11365 0 0 0 35872 62 0 0 25 0 1 0 1793723053 48869376 11038 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 11931 11038 145 145 0 11786 0
[pid=13373] vsize: 47724
Current children cumulated CPU time (s) 359.36
Current children cumulated vsize (Kb) 49848

[startup+370.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11406 0 0 0 36870 63 0 0 25 0 1 0 1793723053 49549312 11079 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 12097 11079 145 145 0 11952 0
[pid=13373] vsize: 48388
Current children cumulated CPU time (s) 369.35
Current children cumulated vsize (Kb) 50512

[startup+380.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11441 0 0 0 37869 64 0 0 25 0 1 0 1793723053 49684480 11114 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 12130 11114 145 145 0 11985 0
[pid=13373] vsize: 48520
Current children cumulated CPU time (s) 379.35
Current children cumulated vsize (Kb) 50644

[startup+390.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11476 0 0 0 38868 65 0 0 25 0 1 0 1793723053 49819648 11149 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 12163 11149 145 145 0 12018 0
[pid=13373] vsize: 48652
Current children cumulated CPU time (s) 389.35
Current children cumulated vsize (Kb) 50776

[startup+400.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11511 0 0 0 39867 66 0 0 25 0 1 0 1793723053 49954816 11184 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 12196 11184 145 145 0 12051 0
[pid=13373] vsize: 48784
Current children cumulated CPU time (s) 399.35
Current children cumulated vsize (Kb) 50908

[startup+410.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11582 0 0 0 40865 67 0 0 25 0 1 0 1793723053 50233344 11255 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 12264 11255 145 145 0 12119 0
[pid=13373] vsize: 49056
Current children cumulated CPU time (s) 409.34
Current children cumulated vsize (Kb) 51180

[startup+420.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11633 0 0 0 41864 68 0 0 25 0 1 0 1793723053 50434048 11306 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 12313 11306 145 145 0 12168 0
[pid=13373] vsize: 49252
Current children cumulated CPU time (s) 419.34
Current children cumulated vsize (Kb) 51376

[startup+430.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11680 0 0 0 42862 68 0 0 25 0 1 0 1793723053 50610176 11353 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12356 11353 145 145 0 12211 0
[pid=13373] vsize: 49424
Current children cumulated CPU time (s) 429.32
Current children cumulated vsize (Kb) 51548

[startup+440.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11725 0 0 0 43862 69 0 0 25 0 1 0 1793723053 50782208 11398 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12398 11398 145 145 0 12253 0
[pid=13373] vsize: 49592
Current children cumulated CPU time (s) 439.33
Current children cumulated vsize (Kb) 51716

[startup+450.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11780 0 0 0 44861 69 0 0 25 0 1 0 1793723053 50999296 11453 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12451 11453 145 145 0 12306 0
[pid=13373] vsize: 49804
Current children cumulated CPU time (s) 449.32
Current children cumulated vsize (Kb) 51928

[startup+460.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11847 0 0 0 45859 70 0 0 25 0 1 0 1793723053 51257344 11520 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12514 11520 145 145 0 12369 0
[pid=13373] vsize: 50056
Current children cumulated CPU time (s) 459.31
Current children cumulated vsize (Kb) 52180

[startup+470.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11910 0 0 0 46859 70 0 0 25 0 1 0 1793723053 51507200 11583 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12575 11583 145 145 0 12430 0
[pid=13373] vsize: 50300
Current children cumulated CPU time (s) 469.31
Current children cumulated vsize (Kb) 52424

[startup+480.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 11983 0 0 0 47857 71 0 0 25 0 1 0 1793723053 51789824 11656 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 12644 11656 145 145 0 12499 0
[pid=13373] vsize: 50576
Current children cumulated CPU time (s) 479.3
Current children cumulated vsize (Kb) 52700

[startup+490.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12035 0 0 0 48855 72 0 0 25 0 1 0 1793723053 51990528 11708 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12693 11708 145 145 0 12548 0
[pid=13373] vsize: 50772
Current children cumulated CPU time (s) 489.29
Current children cumulated vsize (Kb) 52896

[startup+500.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12091 0 0 0 49855 72 0 0 25 0 1 0 1793723053 52211712 11764 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12747 11764 145 145 0 12602 0
[pid=13373] vsize: 50988
Current children cumulated CPU time (s) 499.29
Current children cumulated vsize (Kb) 53112

[startup+510.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12145 0 0 0 50854 73 0 0 25 0 1 0 1793723053 52420608 11818 4294967295 134512640 135094434 3221224432 3221223088 134561698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12798 11818 145 145 0 12653 0
[pid=13373] vsize: 51192
Current children cumulated CPU time (s) 509.29
Current children cumulated vsize (Kb) 53316

[startup+520.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12196 0 0 0 51853 73 0 0 25 0 1 0 1793723053 52621312 11869 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12847 11869 145 145 0 12702 0
[pid=13373] vsize: 51388
Current children cumulated CPU time (s) 519.28
Current children cumulated vsize (Kb) 53512

[startup+530.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12266 0 0 0 52852 74 0 0 25 0 1 0 1793723053 52895744 11939 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 12914 11939 145 145 0 12769 0
[pid=13373] vsize: 51656
Current children cumulated CPU time (s) 529.28
Current children cumulated vsize (Kb) 53780

[startup+540.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12477 0 0 0 53849 75 0 0 25 0 1 0 1793723053 53735424 12150 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13119 12150 145 145 0 12974 0
[pid=13373] vsize: 52476
Current children cumulated CPU time (s) 539.26
Current children cumulated vsize (Kb) 54600

[startup+550.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12542 0 0 0 54848 76 0 0 25 0 1 0 1793723053 53985280 12215 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13180 12215 145 145 0 13035 0
[pid=13373] vsize: 52720
Current children cumulated CPU time (s) 549.26
Current children cumulated vsize (Kb) 54844

[startup+560.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12625 0 0 0 55846 77 0 0 25 0 1 0 1793723053 54312960 12298 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13260 12298 145 145 0 13115 0
[pid=13373] vsize: 53040
Current children cumulated CPU time (s) 559.25
Current children cumulated vsize (Kb) 55164

[startup+570.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12720 0 0 0 56846 77 0 0 25 0 1 0 1793723053 54685696 12393 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13351 12393 145 145 0 13206 0
[pid=13373] vsize: 53404
Current children cumulated CPU time (s) 569.25
Current children cumulated vsize (Kb) 55528

[startup+580.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12789 0 0 0 57844 78 0 0 25 0 1 0 1793723053 54960128 12462 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 13418 12462 145 145 0 13273 0
[pid=13373] vsize: 53672
Current children cumulated CPU time (s) 579.24
Current children cumulated vsize (Kb) 55796

[startup+590.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12855 0 0 0 58842 79 0 0 25 0 1 0 1793723053 55218176 12528 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13481 12528 145 145 0 13336 0
[pid=13373] vsize: 53924
Current children cumulated CPU time (s) 589.23
Current children cumulated vsize (Kb) 56048

[startup+600.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 12942 0 0 0 59841 79 0 0 25 0 1 0 1793723053 55558144 12615 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13564 12615 145 145 0 13419 0
[pid=13373] vsize: 54256
Current children cumulated CPU time (s) 599.22
Current children cumulated vsize (Kb) 56380

[startup+610.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13009 0 0 0 60840 79 0 0 25 0 1 0 1793723053 55824384 12682 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13629 12682 145 145 0 13484 0
[pid=13373] vsize: 54516
Current children cumulated CPU time (s) 609.21
Current children cumulated vsize (Kb) 56640

[startup+620.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13098 0 0 0 61838 80 0 0 25 0 1 0 1793723053 56172544 12771 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 13714 12771 145 145 0 13569 0
[pid=13373] vsize: 54856
Current children cumulated CPU time (s) 619.2
Current children cumulated vsize (Kb) 56980

[startup+630.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13159 0 0 0 62836 81 0 0 25 0 1 0 1793723053 56414208 12832 4294967295 134512640 135094434 3221224432 3221223088 134561717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 13773 12832 145 145 0 13628 0
[pid=13373] vsize: 55092
Current children cumulated CPU time (s) 629.19
Current children cumulated vsize (Kb) 57216

[startup+640.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13220 0 0 0 63835 82 0 0 25 0 1 0 1793723053 56651776 12893 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 13831 12893 145 145 0 13686 0
[pid=13373] vsize: 55324
Current children cumulated CPU time (s) 639.19
Current children cumulated vsize (Kb) 57448

[startup+650.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13289 0 0 0 64834 83 0 0 25 0 1 0 1793723053 56922112 12962 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13897 12962 145 145 0 13752 0
[pid=13373] vsize: 55588
Current children cumulated CPU time (s) 649.19
Current children cumulated vsize (Kb) 57712

[startup+660.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13365 0 0 0 65833 83 0 0 25 0 1 0 1793723053 57221120 13038 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 13970 13038 145 145 0 13825 0
[pid=13373] vsize: 55880
Current children cumulated CPU time (s) 659.18
Current children cumulated vsize (Kb) 58004

[startup+670.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13416 0 0 0 66832 84 0 0 25 0 1 0 1793723053 57421824 13089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14019 13089 145 145 0 13874 0
[pid=13373] vsize: 56076
Current children cumulated CPU time (s) 669.18
Current children cumulated vsize (Kb) 58200

[startup+680.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13476 0 0 0 67831 84 0 0 25 0 1 0 1793723053 57659392 13149 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14077 13149 145 145 0 13932 0
[pid=13373] vsize: 56308
Current children cumulated CPU time (s) 679.17
Current children cumulated vsize (Kb) 58432

[startup+690.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13541 0 0 0 68830 85 0 0 25 0 1 0 1793723053 57913344 13214 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14139 13214 145 145 0 13994 0
[pid=13373] vsize: 56556
Current children cumulated CPU time (s) 689.17
Current children cumulated vsize (Kb) 58680

[startup+700.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13602 0 0 0 69829 85 0 0 25 0 1 0 1793723053 58155008 13275 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14198 13275 145 145 0 14053 0
[pid=13373] vsize: 56792
Current children cumulated CPU time (s) 699.16
Current children cumulated vsize (Kb) 58916

[startup+710.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13698 0 0 0 70827 86 0 0 25 0 1 0 1793723053 58535936 13371 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14291 13371 145 145 0 14146 0
[pid=13373] vsize: 57164
Current children cumulated CPU time (s) 709.15
Current children cumulated vsize (Kb) 59288

[startup+720.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13750 0 0 0 71826 87 0 0 25 0 1 0 1793723053 58736640 13423 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14340 13423 145 145 0 14195 0
[pid=13373] vsize: 57360
Current children cumulated CPU time (s) 719.15
Current children cumulated vsize (Kb) 59484

[startup+730.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13805 0 0 0 72826 87 0 0 25 0 1 0 1793723053 58953728 13478 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14393 13478 145 145 0 14248 0
[pid=13373] vsize: 57572
Current children cumulated CPU time (s) 729.15
Current children cumulated vsize (Kb) 59696

[startup+740.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 13990 0 0 0 73822 89 0 0 25 0 1 0 1793723053 59695104 13663 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14574 13663 145 145 0 14429 0
[pid=13373] vsize: 58296
Current children cumulated CPU time (s) 739.13
Current children cumulated vsize (Kb) 60420

[startup+750.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 14414 0 0 0 74815 92 0 0 25 0 1 0 1793723053 61407232 14087 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 14992 14087 145 145 0 14847 0
[pid=13373] vsize: 59968
Current children cumulated CPU time (s) 749.09
Current children cumulated vsize (Kb) 62092

[startup+760.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 14770 0 0 0 75808 94 0 0 25 0 1 0 1793723053 62849024 14443 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 15344 14443 145 145 0 15199 0
[pid=13373] vsize: 61376
Current children cumulated CPU time (s) 759.04
Current children cumulated vsize (Kb) 63500

[startup+770.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 14904 0 0 0 76806 95 0 0 25 0 1 0 1793723053 63389696 14577 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 15476 14577 145 145 0 15331 0
[pid=13373] vsize: 61904
Current children cumulated CPU time (s) 769.03
Current children cumulated vsize (Kb) 64028

[startup+780.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 14980 0 0 0 77804 96 0 0 25 0 1 0 1793723053 63692800 14653 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 15550 14653 145 145 0 15405 0
[pid=13373] vsize: 62200
Current children cumulated CPU time (s) 779.02
Current children cumulated vsize (Kb) 64324

[startup+790.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 15085 0 0 0 78802 97 0 0 25 0 1 0 1793723053 64110592 14758 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 15652 14758 145 145 0 15507 0
[pid=13373] vsize: 62608
Current children cumulated CPU time (s) 789.01
Current children cumulated vsize (Kb) 64732

[startup+800.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 15173 0 0 0 79801 98 0 0 25 0 1 0 1793723053 65507328 14846 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 15993 14846 145 145 0 15848 0
[pid=13373] vsize: 63972
Current children cumulated CPU time (s) 799.01
Current children cumulated vsize (Kb) 66096

[startup+810.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 15294 0 0 0 80799 99 0 0 25 0 1 0 1793723053 65986560 14967 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 16110 14967 145 145 0 15965 0
[pid=13373] vsize: 64440
Current children cumulated CPU time (s) 809
Current children cumulated vsize (Kb) 66564

[startup+820.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 15399 0 0 0 81798 100 0 0 25 0 1 0 1793723053 66392064 15072 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 16209 15072 145 145 0 16064 0
[pid=13373] vsize: 64836
Current children cumulated CPU time (s) 819
Current children cumulated vsize (Kb) 66960

[startup+830.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 15490 0 0 0 82796 100 0 0 25 0 1 0 1793723053 66752512 15163 4294967295 134512640 135094434 3221224432 3221223044 134563036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 16297 15163 145 145 0 16152 0
[pid=13373] vsize: 65188
Current children cumulated CPU time (s) 828.98
Current children cumulated vsize (Kb) 67312

[startup+840.054 s]
Raw data (loadavg): 1.00 0.99 0.91 1/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) T 13369 13369 1333 0 -1 0 15569 0 0 0 83795 101 0 0 25 0 1 0 1793723053 67067904 15242 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13373/statm): 16374 15242 145 145 0 16229 0
[pid=13373] vsize: 65496
Current children cumulated CPU time (s) 838.98
Current children cumulated vsize (Kb) 67620

[startup+850.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 15659 0 0 0 84794 102 0 0 25 0 1 0 1793723053 67420160 15332 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 16460 15332 145 145 0 16315 0
[pid=13373] vsize: 65840
Current children cumulated CPU time (s) 848.98
Current children cumulated vsize (Kb) 67964

[startup+860.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 15815 0 0 0 85790 103 0 0 25 0 1 0 1793723053 68063232 15488 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 16617 15488 145 145 0 16472 0
[pid=13373] vsize: 66468
Current children cumulated CPU time (s) 858.95
Current children cumulated vsize (Kb) 68592

[startup+870.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 15889 0 0 0 86789 104 0 0 25 0 1 0 1793723053 68354048 15562 4294967295 134512640 135094434 3221224432 3221223056 134557587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 16688 15562 145 145 0 16543 0
[pid=13373] vsize: 66752
Current children cumulated CPU time (s) 868.95
Current children cumulated vsize (Kb) 68876

[startup+880.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 16034 0 0 0 87786 105 0 0 25 0 1 0 1793723053 68931584 15707 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 16829 15707 145 145 0 16684 0
[pid=13373] vsize: 67316
Current children cumulated CPU time (s) 878.93
Current children cumulated vsize (Kb) 69440

[startup+890.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 16306 0 0 0 88782 106 0 0 25 0 1 0 1793723053 70033408 15979 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 17098 15979 145 145 0 16953 0
[pid=13373] vsize: 68392
Current children cumulated CPU time (s) 888.9
Current children cumulated vsize (Kb) 70516

[startup+900.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 16503 0 0 0 89779 108 0 0 25 0 1 0 1793723053 70819840 16176 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 17290 16176 145 145 0 17145 0
[pid=13373] vsize: 69160
Current children cumulated CPU time (s) 898.89
Current children cumulated vsize (Kb) 71284

[startup+910.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 16731 0 0 0 90775 110 0 0 25 0 1 0 1793723053 71737344 16404 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 17514 16404 145 145 0 17369 0
[pid=13373] vsize: 70056
Current children cumulated CPU time (s) 908.87
Current children cumulated vsize (Kb) 72180

[startup+920.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 16898 0 0 0 91772 112 0 0 25 0 1 0 1793723053 72404992 16571 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 17677 16571 145 145 0 17532 0
[pid=13373] vsize: 70708
Current children cumulated CPU time (s) 918.86
Current children cumulated vsize (Kb) 72832

[startup+930.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 17454 0 0 0 92762 116 0 0 25 0 1 0 1793723053 74645504 17127 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 18224 17127 145 145 0 18079 0
[pid=13373] vsize: 72896
Current children cumulated CPU time (s) 928.8
Current children cumulated vsize (Kb) 75020

[startup+940.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 17637 0 0 0 93759 118 0 0 25 0 1 0 1793723053 75378688 17310 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 18403 17310 145 145 0 18258 0
[pid=13373] vsize: 73612
Current children cumulated CPU time (s) 938.79
Current children cumulated vsize (Kb) 75736

[startup+950.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 17734 0 0 0 94757 119 0 0 25 0 1 0 1793723053 75759616 17407 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 18496 17407 145 145 0 18351 0
[pid=13373] vsize: 73984
Current children cumulated CPU time (s) 948.78
Current children cumulated vsize (Kb) 76108

[startup+960.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 17827 0 0 0 95755 120 0 0 25 0 1 0 1793723053 76132352 17500 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 18587 17500 145 145 0 18442 0
[pid=13373] vsize: 74348
Current children cumulated CPU time (s) 958.77
Current children cumulated vsize (Kb) 76472

[startup+970.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 17995 0 0 0 96752 122 0 0 25 0 1 0 1793723053 76800000 17668 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 18750 17668 145 145 0 18605 0
[pid=13373] vsize: 75000
Current children cumulated CPU time (s) 968.76
Current children cumulated vsize (Kb) 77124

[startup+980.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 18193 0 0 0 97748 124 0 0 25 0 1 0 1793723053 77598720 17866 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 18945 17866 145 145 0 18800 0
[pid=13373] vsize: 75780
Current children cumulated CPU time (s) 978.74
Current children cumulated vsize (Kb) 77904

[startup+990.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 18410 0 0 0 98744 125 0 0 25 0 1 0 1793723053 78467072 18083 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 19157 18083 145 145 0 19012 0
[pid=13373] vsize: 76628
Current children cumulated CPU time (s) 988.71
Current children cumulated vsize (Kb) 78752

[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 18536 0 0 0 99742 126 0 0 25 0 1 0 1793723053 78966784 18209 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 19279 18209 145 145 0 19134 0
[pid=13373] vsize: 77116
Current children cumulated CPU time (s) 998.7
Current children cumulated vsize (Kb) 79240

[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 18601 0 0 0 100741 127 0 0 25 0 1 0 1793723053 79224832 18274 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 19342 18274 145 145 0 19197 0
[pid=13373] vsize: 77368
Current children cumulated CPU time (s) 1008.7
Current children cumulated vsize (Kb) 79492

[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 18870 0 0 0 101737 129 0 0 25 0 1 0 1793723053 80297984 18543 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 19604 18543 145 145 0 19459 0
[pid=13373] vsize: 78416
Current children cumulated CPU time (s) 1018.68
Current children cumulated vsize (Kb) 80540

[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 19121 0 0 0 102732 131 0 0 25 0 1 0 1793723053 81309696 18794 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 19851 18794 145 145 0 19706 0
[pid=13373] vsize: 79404
Current children cumulated CPU time (s) 1028.65
Current children cumulated vsize (Kb) 81528

[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 19495 0 0 0 103725 133 0 0 25 0 1 0 1793723053 82808832 19168 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 20217 19168 145 145 0 20072 0
[pid=13373] vsize: 80868
Current children cumulated CPU time (s) 1038.6
Current children cumulated vsize (Kb) 82992

[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 19658 0 0 0 104721 134 0 0 25 0 1 0 1793723053 83460096 19331 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 20376 19331 145 145 0 20231 0
[pid=13373] vsize: 81504
Current children cumulated CPU time (s) 1048.57
Current children cumulated vsize (Kb) 83628

[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 19764 0 0 0 105719 135 0 0 25 0 1 0 1793723053 83881984 19437 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 20479 19437 145 145 0 20334 0
[pid=13373] vsize: 81916
Current children cumulated CPU time (s) 1058.56
Current children cumulated vsize (Kb) 84040

[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 19872 0 0 0 106717 136 0 0 25 0 1 0 1793723053 84312064 19545 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 20584 19545 145 145 0 20439 0
[pid=13373] vsize: 82336
Current children cumulated CPU time (s) 1068.55
Current children cumulated vsize (Kb) 84460

[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 20015 0 0 0 107715 138 0 0 25 0 1 0 1793723053 84889600 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 20725 19688 145 145 0 20580 0
[pid=13373] vsize: 82900
Current children cumulated CPU time (s) 1078.55
Current children cumulated vsize (Kb) 85024

[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 20082 0 0 0 108713 139 0 0 25 0 1 0 1793723053 85151744 19755 4294967295 134512640 135094434 3221224432 3221223084 134561527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 20789 19755 145 145 0 20644 0
[pid=13373] vsize: 83156
Current children cumulated CPU time (s) 1088.54
Current children cumulated vsize (Kb) 85280

[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 20282 0 0 0 109709 140 0 0 25 0 1 0 1793723053 85954560 19955 4294967295 134512640 135094434 3221224432 3221223024 134552003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 20985 19955 145 145 0 20840 0
[pid=13373] vsize: 83940
Current children cumulated CPU time (s) 1098.51
Current children cumulated vsize (Kb) 86064

[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 20701 0 0 0 110701 144 0 0 25 0 1 0 1793723053 87646208 20374 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 21398 20374 145 145 0 21253 0
[pid=13373] vsize: 85592
Current children cumulated CPU time (s) 1108.47
Current children cumulated vsize (Kb) 87716

[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 21066 0 0 0 111693 147 0 0 25 0 1 0 1793723053 89116672 20739 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 21757 20739 145 145 0 21612 0
[pid=13373] vsize: 87028
Current children cumulated CPU time (s) 1118.42
Current children cumulated vsize (Kb) 89152

[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 21223 0 0 0 112690 149 0 0 25 0 1 0 1793723053 89747456 20896 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 21911 20896 145 145 0 21766 0
[pid=13373] vsize: 87644
Current children cumulated CPU time (s) 1128.41
Current children cumulated vsize (Kb) 89768

[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 21426 0 0 0 113686 151 0 0 25 0 1 0 1793723053 90578944 21099 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 22114 21099 145 145 0 21969 0
[pid=13373] vsize: 88456
Current children cumulated CPU time (s) 1138.39
Current children cumulated vsize (Kb) 90580

[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) T 13369 13369 1333 0 -1 0 21629 0 0 0 114682 153 0 0 25 0 1 0 1793723053 91389952 21302 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13373/statm): 22312 21302 145 145 0 22167 0
[pid=13373] vsize: 89248
Current children cumulated CPU time (s) 1148.37
Current children cumulated vsize (Kb) 91372

[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 21976 0 0 0 115676 155 0 0 25 0 1 0 1793723053 92790784 21649 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 22654 21649 145 145 0 22509 0
[pid=13373] vsize: 90616
Current children cumulated CPU time (s) 1158.33
Current children cumulated vsize (Kb) 92740

[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 22243 0 0 0 116670 157 0 0 25 0 1 0 1793723053 93868032 21916 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 22917 21916 145 145 0 22772 0
[pid=13373] vsize: 91668
Current children cumulated CPU time (s) 1168.29
Current children cumulated vsize (Kb) 93792

[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 22655 0 0 0 117664 160 0 0 25 0 1 0 1793723053 95535104 22328 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 23324 22328 145 145 0 23179 0
[pid=13373] vsize: 93296
Current children cumulated CPU time (s) 1178.26
Current children cumulated vsize (Kb) 95420

[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 22935 0 0 0 118659 162 0 0 25 0 1 0 1793723053 96665600 22608 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 23600 22608 145 145 0 23455 0
[pid=13373] vsize: 94400
Current children cumulated CPU time (s) 1188.23
Current children cumulated vsize (Kb) 96524

[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 23231 0 0 0 119653 164 0 0 25 0 1 0 1793723053 97861632 22904 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13373/statm): 23892 22904 145 145 0 23747 0
[pid=13373] vsize: 95568
Current children cumulated CPU time (s) 1198.19
Current children cumulated vsize (Kb) 97692

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 23527 0 0 0 120647 166 0 0 25 0 1 0 1793723053 99057664 23200 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 24184 23200 145 145 0 24039 0
[pid=13373] vsize: 96736
Current children cumulated CPU time (s) 1208.15
Current children cumulated vsize (Kb) 98860



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 13373
Raw data (/proc/13369/stat): 13369 (minisat+_script) S 13368 13369 1333 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793723048 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13369/statm): 531 226 485 147 0 384 0
[pid=13369] vsize: 2124
Raw data (/proc/13373/stat): 13373 (minisat+_64-bit) R 13369 13369 1333 0 -1 0 23527 0 0 0 120647 166 0 0 25 0 1 0 1793723053 99057664 23200 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13373/statm): 24184 23200 145 145 0 24039 0
[pid=13373] vsize: 96736
Current children cumulated CPU time (s) 1208.15
Current children cumulated vsize (Kb) 98860

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1208.19
CPU user time (s): 1206.48
CPU system time (s): 1.71274
CPU usage (%): 99.8401
Max. virtual memory (cumulated for all children) (Kb): 98860