PB'05 competition: run trace

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/23575/stat): 23575 (minisat+_script) R 23574 23575 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841363840 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/23575/statm): 174 3 169 147 0 27 0
[pid=23575] 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=23576
New process pid=23577
New process pid=23578
execve syscall for /bin/sed executable
One traced child (pid=23577) 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=23578) exited with status: 0
One traced child (pid=23576) exited with status: 0
New process pid=23579
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-alu4.b.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 2567 0 0 0 973 10 0 0 25 0 1 0 1841363845 11837440 2547 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 2890 2547 145 145 0 2745 0
[pid=23579] vsize: 11560
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 13684

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 3294 0 0 0 1960 15 0 0 25 0 1 0 1841363845 14823424 3274 4294967295 134512640 135094434 3221224448 3221223040 134551883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 3619 3274 145 145 0 3474 0
[pid=23579] vsize: 14476
Current children cumulated CPU time (s) 19.75
Current children cumulated vsize (Kb) 16600

[startup+30.0056 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 4014 0 0 0 2947 22 0 0 25 0 1 0 1841363845 17756160 3994 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 4335 3994 145 145 0 4190 0
[pid=23579] vsize: 17340
Current children cumulated CPU time (s) 29.69
Current children cumulated vsize (Kb) 19464

[startup+40.0063 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 4333 0 0 0 3942 24 0 0 25 0 1 0 1841363845 19120128 4313 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 4668 4313 145 145 0 4523 0
[pid=23579] vsize: 18672
Current children cumulated CPU time (s) 39.66
Current children cumulated vsize (Kb) 20796

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 4572 0 0 0 4938 26 0 0 25 0 1 0 1841363845 20090880 4552 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 4905 4552 145 145 0 4760 0
[pid=23579] vsize: 19620
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 21744

[startup+60.0086 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 4572 0 0 0 5938 26 0 0 25 0 1 0 1841363845 20090880 4552 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 4905 4552 145 145 0 4760 0
[pid=23579] vsize: 19620
Current children cumulated CPU time (s) 59.64
Current children cumulated vsize (Kb) 21744

[startup+70.0093 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 4572 0 0 0 6939 26 0 0 25 0 1 0 1841363845 20090880 4552 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 4905 4552 145 145 0 4760 0
[pid=23579] vsize: 19620
Current children cumulated CPU time (s) 69.65
Current children cumulated vsize (Kb) 21744

[startup+80.01 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 4653 0 0 0 7937 27 0 0 25 0 1 0 1841363845 20426752 4633 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 4987 4633 145 145 0 4842 0
[pid=23579] vsize: 19948
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 22072

[startup+90.0107 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 4982 0 0 0 8931 29 0 0 25 0 1 0 1841363845 21762048 4962 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 5313 4962 145 145 0 5168 0
[pid=23579] vsize: 21252
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 23376

[startup+100.011 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5284 0 0 0 9924 32 0 0 25 0 1 0 1841363845 22986752 5264 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 5612 5264 145 145 0 5467 0
[pid=23579] vsize: 22448
Current children cumulated CPU time (s) 99.56
Current children cumulated vsize (Kb) 24572

[startup+110.013 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5587 0 0 0 10916 36 0 0 25 0 1 0 1841363845 24211456 5567 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 5911 5567 145 145 0 5766 0
[pid=23579] vsize: 23644
Current children cumulated CPU time (s) 109.52
Current children cumulated vsize (Kb) 25768

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5862 0 0 0 11912 38 0 0 25 0 1 0 1841363845 25329664 5842 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6184 5842 145 145 0 6039 0
[pid=23579] vsize: 24736
Current children cumulated CPU time (s) 119.5
Current children cumulated vsize (Kb) 26860

[startup+130.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5862 0 0 0 12911 39 0 0 25 0 1 0 1841363845 25329664 5842 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6184 5842 145 145 0 6039 0
[pid=23579] vsize: 24736
Current children cumulated CPU time (s) 129.5
Current children cumulated vsize (Kb) 26860

[startup+140.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5862 0 0 0 13911 39 0 0 25 0 1 0 1841363845 25329664 5842 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6184 5842 145 145 0 6039 0
[pid=23579] vsize: 24736
Current children cumulated CPU time (s) 139.5
Current children cumulated vsize (Kb) 26860

[startup+150.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5862 0 0 0 14911 39 0 0 25 0 1 0 1841363845 25329664 5842 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6184 5842 145 145 0 6039 0
[pid=23579] vsize: 24736
Current children cumulated CPU time (s) 149.5
Current children cumulated vsize (Kb) 26860

[startup+160.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5862 0 0 0 15910 40 0 0 25 0 1 0 1841363845 25329664 5842 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6184 5842 145 145 0 6039 0
[pid=23579] vsize: 24736
Current children cumulated CPU time (s) 159.5
Current children cumulated vsize (Kb) 26860

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5863 0 0 0 16910 40 0 0 25 0 1 0 1841363845 25329664 5843 4294967295 134512640 135094434 3221224448 3221223200 134559163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6184 5843 145 145 0 6039 0
[pid=23579] vsize: 24736
Current children cumulated CPU time (s) 169.5
Current children cumulated vsize (Kb) 26860

[startup+180.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5897 0 0 0 17909 41 0 0 25 0 1 0 1841363845 25591808 5877 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6248 5877 145 145 0 6103 0
[pid=23579] vsize: 24992
Current children cumulated CPU time (s) 179.5
Current children cumulated vsize (Kb) 27116

[startup+190.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 5900 0 0 0 18909 41 0 0 25 0 1 0 1841363845 25591808 5880 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6248 5880 145 145 0 6103 0
[pid=23579] vsize: 24992
Current children cumulated CPU time (s) 189.5
Current children cumulated vsize (Kb) 27116

[startup+200.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 6227 0 0 0 19903 45 0 0 25 0 1 0 1841363845 26918912 6207 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 6572 6207 145 145 0 6427 0
[pid=23579] vsize: 26288
Current children cumulated CPU time (s) 199.48
Current children cumulated vsize (Kb) 28412

[startup+210.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 6734 0 0 0 20893 50 0 0 25 0 1 0 1841363845 28983296 6714 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 7076 6714 145 145 0 6931 0
[pid=23579] vsize: 28304
Current children cumulated CPU time (s) 209.43
Current children cumulated vsize (Kb) 30428

[startup+220.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7159 0 0 0 21883 53 0 0 25 0 1 0 1841363845 30715904 7139 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 7499 7139 145 145 0 7354 0
[pid=23579] vsize: 29996
Current children cumulated CPU time (s) 219.36
Current children cumulated vsize (Kb) 32120

[startup+230.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 22875 57 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 229.32
Current children cumulated vsize (Kb) 33840

[startup+240.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 23874 57 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 239.31
Current children cumulated vsize (Kb) 33840

[startup+250.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 24874 58 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 249.32
Current children cumulated vsize (Kb) 33840

[startup+260.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 25874 58 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 259.32
Current children cumulated vsize (Kb) 33840

[startup+270.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 26874 59 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 269.33
Current children cumulated vsize (Kb) 33840

[startup+280.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 27873 59 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 279.32
Current children cumulated vsize (Kb) 33840

[startup+290.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 28873 60 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 289.33
Current children cumulated vsize (Kb) 33840

[startup+300.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 29873 60 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 299.33
Current children cumulated vsize (Kb) 33840

[startup+310.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7591 0 0 0 30873 60 0 0 25 0 1 0 1841363845 32477184 7571 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 7929 7571 145 145 0 7784 0
[pid=23579] vsize: 31716
Current children cumulated CPU time (s) 309.33
Current children cumulated vsize (Kb) 33840

[startup+320.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7666 0 0 0 31872 61 0 0 25 0 1 0 1841363845 32788480 7646 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 8005 7646 145 145 0 7860 0
[pid=23579] vsize: 32020
Current children cumulated CPU time (s) 319.33
Current children cumulated vsize (Kb) 34144

[startup+330.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 7970 0 0 0 32865 65 0 0 25 0 1 0 1841363845 34033664 7950 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 8309 7950 145 145 0 8164 0
[pid=23579] vsize: 33236
Current children cumulated CPU time (s) 329.3
Current children cumulated vsize (Kb) 35360

[startup+340.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 8297 0 0 0 33859 68 0 0 25 0 1 0 1841363845 35377152 8277 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 8637 8277 145 145 0 8492 0
[pid=23579] vsize: 34548
Current children cumulated CPU time (s) 339.27
Current children cumulated vsize (Kb) 36672

[startup+350.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 8577 0 0 0 34854 70 0 0 25 0 1 0 1841363845 36528128 8557 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 8918 8557 145 145 0 8773 0
[pid=23579] vsize: 35672
Current children cumulated CPU time (s) 349.24
Current children cumulated vsize (Kb) 37796

[startup+360.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 8849 0 0 0 35847 72 0 0 25 0 1 0 1841363845 37642240 8829 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 9190 8829 145 145 0 9045 0
[pid=23579] vsize: 36760
Current children cumulated CPU time (s) 359.19
Current children cumulated vsize (Kb) 38884

[startup+370.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 9174 0 0 0 36841 75 0 0 25 0 1 0 1841363845 38969344 9154 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 9514 9154 145 145 0 9369 0
[pid=23579] vsize: 38056
Current children cumulated CPU time (s) 369.16
Current children cumulated vsize (Kb) 40180

[startup+380.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 9418 0 0 0 37836 78 0 0 25 0 1 0 1841363845 39976960 9398 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 9760 9398 145 145 0 9615 0
[pid=23579] vsize: 39040
Current children cumulated CPU time (s) 379.14
Current children cumulated vsize (Kb) 41164

[startup+390.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 9719 0 0 0 38829 80 0 0 25 0 1 0 1841363845 41209856 9699 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 10061 9699 145 145 0 9916 0
[pid=23579] vsize: 40244
Current children cumulated CPU time (s) 389.09
Current children cumulated vsize (Kb) 42368

[startup+400.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10056 0 0 0 39823 83 0 0 25 0 1 0 1841363845 42582016 10036 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 10396 10036 145 145 0 10251 0
[pid=23579] vsize: 41584
Current children cumulated CPU time (s) 399.06
Current children cumulated vsize (Kb) 43708

[startup+410.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10334 0 0 0 40819 85 0 0 25 0 1 0 1841363845 43708416 10314 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 10671 10314 145 145 0 10526 0
[pid=23579] vsize: 42684
Current children cumulated CPU time (s) 409.04
Current children cumulated vsize (Kb) 44808

[startup+420.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10562 0 0 0 41814 87 0 0 25 0 1 0 1841363845 44658688 10542 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 10903 10542 145 145 0 10758 0
[pid=23579] vsize: 43612
Current children cumulated CPU time (s) 419.01
Current children cumulated vsize (Kb) 45736

[startup+430.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10872 0 0 0 42808 89 0 0 25 0 1 0 1841363845 45920256 10852 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10852 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 428.97
Current children cumulated vsize (Kb) 46968

[startup+440.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10872 0 0 0 43809 89 0 0 25 0 1 0 1841363845 45920256 10852 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10852 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 438.98
Current children cumulated vsize (Kb) 46968

[startup+450.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10874 0 0 0 44809 89 0 0 25 0 1 0 1841363845 45920256 10854 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10854 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 448.98
Current children cumulated vsize (Kb) 46968

[startup+460.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10874 0 0 0 45809 89 0 0 25 0 1 0 1841363845 45920256 10854 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10854 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 458.98
Current children cumulated vsize (Kb) 46968

[startup+470.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 46809 89 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 468.98
Current children cumulated vsize (Kb) 46968

[startup+480.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 47808 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 478.98
Current children cumulated vsize (Kb) 46968

[startup+490.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 48808 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 488.98
Current children cumulated vsize (Kb) 46968

[startup+500.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 49808 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 498.98
Current children cumulated vsize (Kb) 46968

[startup+510.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 50808 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 508.98
Current children cumulated vsize (Kb) 46968

[startup+520.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 51808 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 518.98
Current children cumulated vsize (Kb) 46968

[startup+530.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 52809 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 528.99
Current children cumulated vsize (Kb) 46968

[startup+540.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 53809 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134558135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 538.99
Current children cumulated vsize (Kb) 46968

[startup+550.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 54809 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223120 134555837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 548.99
Current children cumulated vsize (Kb) 46968

[startup+560.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 55809 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 558.99
Current children cumulated vsize (Kb) 46968

[startup+570.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 56809 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 568.99
Current children cumulated vsize (Kb) 46968

[startup+580.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 57810 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 579
Current children cumulated vsize (Kb) 46968

[startup+590.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 58810 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 589
Current children cumulated vsize (Kb) 46968

[startup+600.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 59810 90 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 599
Current children cumulated vsize (Kb) 46968

[startup+610.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10875 0 0 0 60810 91 0 0 25 0 1 0 1841363845 45920256 10855 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10855 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 609.01
Current children cumulated vsize (Kb) 46968

[startup+620.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10877 0 0 0 61810 91 0 0 25 0 1 0 1841363845 45920256 10857 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10857 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 619.01
Current children cumulated vsize (Kb) 46968

[startup+630.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10879 0 0 0 62810 91 0 0 25 0 1 0 1841363845 45920256 10859 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10859 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 629.01
Current children cumulated vsize (Kb) 46968

[startup+640.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 63811 91 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 639.02
Current children cumulated vsize (Kb) 46968

[startup+650.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 64811 91 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 649.02
Current children cumulated vsize (Kb) 46968

[startup+660.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 65811 91 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 659.02
Current children cumulated vsize (Kb) 46968

[startup+670.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 66811 91 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 669.02
Current children cumulated vsize (Kb) 46968

[startup+680.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 67810 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 679.02
Current children cumulated vsize (Kb) 46968

[startup+690.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 68810 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 689.02
Current children cumulated vsize (Kb) 46968

[startup+700.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 69811 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 699.03
Current children cumulated vsize (Kb) 46968

[startup+710.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 70811 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 709.03
Current children cumulated vsize (Kb) 46968

[startup+720.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 71811 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 719.03
Current children cumulated vsize (Kb) 46968

[startup+730.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 72811 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 729.03
Current children cumulated vsize (Kb) 46968

[startup+740.074 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 73812 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 739.04
Current children cumulated vsize (Kb) 46968

[startup+750.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 74812 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 749.04
Current children cumulated vsize (Kb) 46968

[startup+760.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 75812 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 759.04
Current children cumulated vsize (Kb) 46968

[startup+770.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 76812 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 769.04
Current children cumulated vsize (Kb) 46968

[startup+780.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 77812 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 779.04
Current children cumulated vsize (Kb) 46968

[startup+790.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 78813 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 789.05
Current children cumulated vsize (Kb) 46968

[startup+800.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 79813 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 799.05
Current children cumulated vsize (Kb) 46968

[startup+810.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10881 0 0 0 80813 92 0 0 25 0 1 0 1841363845 45920256 10861 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10861 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 809.05
Current children cumulated vsize (Kb) 46968

[startup+820.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10884 0 0 0 81813 92 0 0 25 0 1 0 1841363845 45920256 10864 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11211 10864 145 145 0 11066 0
[pid=23579] vsize: 44844
Current children cumulated CPU time (s) 819.05
Current children cumulated vsize (Kb) 46968

[startup+830.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10886 0 0 0 82814 92 0 0 25 0 1 0 1841363845 46182400 10866 4294967295 134512640 135094434 3221224448 3221223104 134557987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10866 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 829.06
Current children cumulated vsize (Kb) 47224

[startup+840.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 83813 92 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 839.05
Current children cumulated vsize (Kb) 47224

[startup+850.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 84814 92 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 849.06
Current children cumulated vsize (Kb) 47224

[startup+860.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 85814 92 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 859.06
Current children cumulated vsize (Kb) 47224

[startup+870.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 86813 94 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 869.07
Current children cumulated vsize (Kb) 47224

[startup+880.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 87812 95 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 879.07
Current children cumulated vsize (Kb) 47224

[startup+890.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 88812 95 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 889.07
Current children cumulated vsize (Kb) 47224

[startup+900.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 89812 95 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 899.07
Current children cumulated vsize (Kb) 47224

[startup+910.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 90812 95 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 909.07
Current children cumulated vsize (Kb) 47224

[startup+920.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 91811 96 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 919.07
Current children cumulated vsize (Kb) 47224

[startup+930.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 92811 96 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 929.07
Current children cumulated vsize (Kb) 47224

[startup+940.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 93812 96 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 939.08
Current children cumulated vsize (Kb) 47224

[startup+950.091 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 94812 96 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 949.08
Current children cumulated vsize (Kb) 47224

[startup+960.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 95812 97 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 959.09
Current children cumulated vsize (Kb) 47224

[startup+970.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 96812 97 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 969.09
Current children cumulated vsize (Kb) 47224

[startup+980.093 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 97812 97 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 979.09
Current children cumulated vsize (Kb) 47224

[startup+990.094 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 98812 97 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 989.09
Current children cumulated vsize (Kb) 47224

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 99812 97 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 999.09
Current children cumulated vsize (Kb) 47224

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 100813 97 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1009.1
Current children cumulated vsize (Kb) 47224

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 101812 98 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1019.1
Current children cumulated vsize (Kb) 47224

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 102812 98 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1029.1
Current children cumulated vsize (Kb) 47224

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 103812 98 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1039.1
Current children cumulated vsize (Kb) 47224

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 104812 98 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1049.1
Current children cumulated vsize (Kb) 47224

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 105812 98 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1059.1
Current children cumulated vsize (Kb) 47224

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 106812 98 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223072 134557724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1069.1
Current children cumulated vsize (Kb) 47224

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 107813 98 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134558292 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1079.11
Current children cumulated vsize (Kb) 47224

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 108813 98 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223060 134563145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1089.11
Current children cumulated vsize (Kb) 47224

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 109813 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1099.12
Current children cumulated vsize (Kb) 47224

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 110813 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1109.12
Current children cumulated vsize (Kb) 47224

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 111813 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1119.12
Current children cumulated vsize (Kb) 47224

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 112814 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1129.13
Current children cumulated vsize (Kb) 47224

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 113814 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1139.13
Current children cumulated vsize (Kb) 47224

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 114814 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1149.13
Current children cumulated vsize (Kb) 47224

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 115814 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1159.13
Current children cumulated vsize (Kb) 47224

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 116814 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1169.13
Current children cumulated vsize (Kb) 47224

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 117814 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1179.13
Current children cumulated vsize (Kb) 47224

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 118815 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1189.14
Current children cumulated vsize (Kb) 47224

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 119815 99 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1199.14
Current children cumulated vsize (Kb) 47224

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 120815 100 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1209.15
Current children cumulated vsize (Kb) 47224



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 23579
Raw data (/proc/23575/stat): 23575 (minisat+_script) S 23574 23575 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841363840 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23575/statm): 531 226 485 147 0 384 0
[pid=23575] vsize: 2124
Raw data (/proc/23579/stat): 23579 (minisat+_64-bit) R 23575 23575 20728 0 -1 0 10887 0 0 0 120815 100 0 0 25 0 1 0 1841363845 46182400 10867 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23579/statm): 11275 10867 145 145 0 11130 0
[pid=23579] vsize: 45100
Current children cumulated CPU time (s) 1209.15
Current children cumulated vsize (Kb) 47224

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1209.18
CPU user time (s): 1208.16
CPU system time (s): 1.02284
CPU usage (%): 99.9207
Max. virtual memory (cumulated for all children) (Kb): 47224
Name	submitted/manquinho/logic-synthesis/normalized-alu4.b.opb
MD5SUM	db06e7fbd4f70a4af68f8f196fdb3636
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50
Optimality of the best value was proved	NO
Number of terms in the objective function	808
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	808
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	808
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1195.2
Number of variables	807
Total number of constraints	1838
Number of constraints which are clauses	1823
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Some explanations

General information on the benchmark

Trace number 917

Launcher Data

Solver Data

Watcher Data

Verifier Data
