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/29041/stat): 29041 (minisat+_script) R 29040 29041 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784101349 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/29041/statm): 174 3 169 147 0 27 0
[pid=29041] 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=29042
New process pid=29043
New process pid=29044
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
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=29044) exited with status: 0
One traced child (pid=29043) exited with status: 0
One traced child (pid=29042) exited with status: 0
New process pid=29045
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-ii32d2.opb

[startup+10.0036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 3142 0 0 0 967 13 0 0 25 0 1 0 1784101354 13459456 3028 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29045/statm): 3286 3028 145 145 0 3141 0
[pid=29045] vsize: 13144
Current children cumulated CPU time (s) 9.8
Current children cumulated vsize (Kb) 15268

[startup+20.0051 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 3539 0 0 0 1959 17 0 0 25 0 1 0 1784101354 15110144 3425 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 3689 3425 145 145 0 3544 0
[pid=29045] vsize: 14756
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 16880

[startup+30.0067 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 3872 0 0 0 2952 20 0 0 25 0 1 0 1784101354 16470016 3758 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29045/statm): 4021 3758 145 145 0 3876 0
[pid=29045] vsize: 16084
Current children cumulated CPU time (s) 29.72
Current children cumulated vsize (Kb) 18208

[startup+40.0073 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 4130 0 0 0 3947 22 0 0 25 0 1 0 1784101354 17522688 4016 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29045/statm): 4278 4016 145 145 0 4133 0
[pid=29045] vsize: 17112
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 19236

[startup+50.0088 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 4364 0 0 0 4943 25 0 0 25 0 1 0 1784101354 18558976 4250 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 4531 4250 145 145 0 4386 0
[pid=29045] vsize: 18124
Current children cumulated CPU time (s) 49.68
Current children cumulated vsize (Kb) 20248

[startup+60.0094 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 4568 0 0 0 5939 26 0 0 25 0 1 0 1784101354 19390464 4454 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 4734 4454 145 145 0 4589 0
[pid=29045] vsize: 18936
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 21060

[startup+70.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 4765 0 0 0 6934 28 0 0 25 0 1 0 1784101354 20201472 4651 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 4932 4651 145 145 0 4787 0
[pid=29045] vsize: 19728
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 21852

[startup+80.0115 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 5033 0 0 0 7929 30 0 0 25 0 1 0 1784101354 21319680 4919 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 5205 4919 145 145 0 5060 0
[pid=29045] vsize: 20820
Current children cumulated CPU time (s) 79.59
Current children cumulated vsize (Kb) 22944

[startup+90.0121 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 5284 0 0 0 8926 32 0 0 25 0 1 0 1784101354 22405120 5170 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 5470 5170 145 145 0 5325 0
[pid=29045] vsize: 21880
Current children cumulated CPU time (s) 89.58
Current children cumulated vsize (Kb) 24004

[startup+100.013 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 5475 0 0 0 9923 33 0 0 25 0 1 0 1784101354 23179264 5361 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 5659 5361 145 145 0 5514 0
[pid=29045] vsize: 22636
Current children cumulated CPU time (s) 99.56
Current children cumulated vsize (Kb) 24760

[startup+110.013 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 5648 0 0 0 10920 34 0 0 25 0 1 0 1784101354 23875584 5534 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 5829 5534 145 145 0 5684 0
[pid=29045] vsize: 23316
Current children cumulated CPU time (s) 109.54
Current children cumulated vsize (Kb) 25440

[startup+120.014 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 5843 0 0 0 11918 35 0 0 25 0 1 0 1784101354 24727552 5729 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 6037 5729 145 145 0 5892 0
[pid=29045] vsize: 24148
Current children cumulated CPU time (s) 119.53
Current children cumulated vsize (Kb) 26272

[startup+130.014 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 6034 0 0 0 12915 36 0 0 25 0 1 0 1784101354 25583616 5920 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 6246 5920 145 145 0 6101 0
[pid=29045] vsize: 24984
Current children cumulated CPU time (s) 129.51
Current children cumulated vsize (Kb) 27108

[startup+140.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 6185 0 0 0 13914 37 0 0 25 0 1 0 1784101354 26329088 6071 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 6428 6071 145 145 0 6283 0
[pid=29045] vsize: 25712
Current children cumulated CPU time (s) 139.51
Current children cumulated vsize (Kb) 27836

[startup+150.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 6326 0 0 0 14912 38 0 0 25 0 1 0 1784101354 26918912 6212 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 6572 6212 145 145 0 6427 0
[pid=29045] vsize: 26288
Current children cumulated CPU time (s) 149.5
Current children cumulated vsize (Kb) 28412

[startup+160.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 6452 0 0 0 15909 39 0 0 25 0 1 0 1784101354 27439104 6338 4294967295 134512640 135094434 3221224448 3221223104 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 6699 6338 145 145 0 6554 0
[pid=29045] vsize: 26796
Current children cumulated CPU time (s) 159.48
Current children cumulated vsize (Kb) 28920

[startup+170.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 6609 0 0 0 16907 40 0 0 25 0 1 0 1784101354 28127232 6495 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 6867 6495 145 145 0 6722 0
[pid=29045] vsize: 27468
Current children cumulated CPU time (s) 169.47
Current children cumulated vsize (Kb) 29592

[startup+180.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 6783 0 0 0 17906 41 0 0 25 0 1 0 1784101354 28930048 6669 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 7063 6669 145 145 0 6918 0
[pid=29045] vsize: 28252
Current children cumulated CPU time (s) 179.47
Current children cumulated vsize (Kb) 30376

[startup+190.018 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 6931 0 0 0 18904 42 0 0 25 0 1 0 1784101354 29544448 6817 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 7213 6817 145 145 0 7068 0
[pid=29045] vsize: 28852
Current children cumulated CPU time (s) 189.46
Current children cumulated vsize (Kb) 30976

[startup+200.019 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 7122 0 0 0 19902 43 0 0 25 0 1 0 1784101354 30355456 7008 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 7411 7008 145 145 0 7266 0
[pid=29045] vsize: 29644
Current children cumulated CPU time (s) 199.45
Current children cumulated vsize (Kb) 31768

[startup+210.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 7262 0 0 0 20900 44 0 0 25 0 1 0 1784101354 30965760 7148 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29045/statm): 7560 7148 145 145 0 7415 0
[pid=29045] vsize: 30240
Current children cumulated CPU time (s) 209.44
Current children cumulated vsize (Kb) 32364

[startup+220.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 7407 0 0 0 21897 46 0 0 25 0 1 0 1784101354 31543296 7293 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 7701 7293 145 145 0 7556 0
[pid=29045] vsize: 30804
Current children cumulated CPU time (s) 219.43
Current children cumulated vsize (Kb) 32928

[startup+230.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 7597 0 0 0 22896 46 0 0 25 0 1 0 1784101354 32448512 7483 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 7922 7483 145 145 0 7777 0
[pid=29045] vsize: 31688
Current children cumulated CPU time (s) 229.42
Current children cumulated vsize (Kb) 33812

[startup+240.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 7781 0 0 0 23894 47 0 0 25 0 1 0 1784101354 33263616 7667 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 8121 7667 145 145 0 7976 0
[pid=29045] vsize: 32484
Current children cumulated CPU time (s) 239.41
Current children cumulated vsize (Kb) 34608

[startup+250.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 7905 0 0 0 24893 48 0 0 25 0 1 0 1784101354 33783808 7791 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 8248 7791 145 145 0 8103 0
[pid=29045] vsize: 32992
Current children cumulated CPU time (s) 249.41
Current children cumulated vsize (Kb) 35116

[startup+260.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 7996 0 0 0 25890 49 0 0 25 0 1 0 1784101354 34144256 7882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 8336 7882 145 145 0 8191 0
[pid=29045] vsize: 33344
Current children cumulated CPU time (s) 259.39
Current children cumulated vsize (Kb) 35468

[startup+270.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8101 0 0 0 26888 50 0 0 25 0 1 0 1784101354 34562048 7987 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 8438 7987 145 145 0 8293 0
[pid=29045] vsize: 33752
Current children cumulated CPU time (s) 269.38
Current children cumulated vsize (Kb) 35876

[startup+280.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8258 0 0 0 27886 51 0 0 25 0 1 0 1784101354 35270656 8144 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 8611 8144 145 145 0 8466 0
[pid=29045] vsize: 34444
Current children cumulated CPU time (s) 279.37
Current children cumulated vsize (Kb) 36568

[startup+290.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8385 0 0 0 28884 53 0 0 25 0 1 0 1784101354 35778560 8271 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 8735 8271 145 145 0 8590 0
[pid=29045] vsize: 34940
Current children cumulated CPU time (s) 289.37
Current children cumulated vsize (Kb) 37064

[startup+300.027 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8529 0 0 0 29883 54 0 0 25 0 1 0 1784101354 36421632 8415 4294967295 134512640 135094434 3221224448 3221223072 134562113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 8892 8415 145 145 0 8747 0
[pid=29045] vsize: 35568
Current children cumulated CPU time (s) 299.37
Current children cumulated vsize (Kb) 37692

[startup+310.027 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8654 0 0 0 30882 54 0 0 25 0 1 0 1784101354 36990976 8540 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9031 8540 145 145 0 8886 0
[pid=29045] vsize: 36124
Current children cumulated CPU time (s) 309.36
Current children cumulated vsize (Kb) 38248

[startup+320.028 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8780 0 0 0 31881 55 0 0 25 0 1 0 1784101354 37548032 8666 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9167 8666 145 145 0 9022 0
[pid=29045] vsize: 36668
Current children cumulated CPU time (s) 319.36
Current children cumulated vsize (Kb) 38792

[startup+330.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8863 0 0 0 32880 55 0 0 25 0 1 0 1784101354 37875712 8749 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9247 8749 145 145 0 9102 0
[pid=29045] vsize: 36988
Current children cumulated CPU time (s) 329.35
Current children cumulated vsize (Kb) 39112

[startup+340.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8966 0 0 0 33878 56 0 0 25 0 1 0 1784101354 38301696 8852 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9351 8852 145 145 0 9206 0
[pid=29045] vsize: 37404
Current children cumulated CPU time (s) 339.34
Current children cumulated vsize (Kb) 39528

[startup+350.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8966 0 0 0 34878 56 0 0 25 0 1 0 1784101354 38301696 8852 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9351 8852 145 145 0 9206 0
[pid=29045] vsize: 37404
Current children cumulated CPU time (s) 349.34
Current children cumulated vsize (Kb) 39528

[startup+360.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8966 0 0 0 35878 56 0 0 25 0 1 0 1784101354 38301696 8852 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29045/statm): 9351 8852 145 145 0 9206 0
[pid=29045] vsize: 37404
Current children cumulated CPU time (s) 359.34
Current children cumulated vsize (Kb) 39528

[startup+370.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8980 0 0 0 36877 56 0 0 25 0 1 0 1784101354 38379520 8866 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9370 8866 145 145 0 9225 0
[pid=29045] vsize: 37480
Current children cumulated CPU time (s) 369.33
Current children cumulated vsize (Kb) 39604

[startup+380.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 8992 0 0 0 37877 56 0 0 25 0 1 0 1784101354 38412288 8878 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9378 8878 145 145 0 9233 0
[pid=29045] vsize: 37512
Current children cumulated CPU time (s) 379.33
Current children cumulated vsize (Kb) 39636

[startup+390.032 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9047 0 0 0 38877 57 0 0 25 0 1 0 1784101354 38838272 8933 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9482 8933 145 145 0 9337 0
[pid=29045] vsize: 37928
Current children cumulated CPU time (s) 389.34
Current children cumulated vsize (Kb) 40052

[startup+400.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9047 0 0 0 39877 57 0 0 25 0 1 0 1784101354 38838272 8933 4294967295 134512640 135094434 3221224448 3221223108 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9482 8933 145 145 0 9337 0
[pid=29045] vsize: 37928
Current children cumulated CPU time (s) 399.34
Current children cumulated vsize (Kb) 40052

[startup+410.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9048 0 0 0 40877 57 0 0 25 0 1 0 1784101354 38838272 8934 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9482 8934 145 145 0 9337 0
[pid=29045] vsize: 37928
Current children cumulated CPU time (s) 409.34
Current children cumulated vsize (Kb) 40052

[startup+420.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9048 0 0 0 41878 57 0 0 25 0 1 0 1784101354 38838272 8934 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9482 8934 145 145 0 9337 0
[pid=29045] vsize: 37928
Current children cumulated CPU time (s) 419.35
Current children cumulated vsize (Kb) 40052

[startup+430.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9048 0 0 0 42878 57 0 0 25 0 1 0 1784101354 38838272 8934 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9482 8934 145 145 0 9337 0
[pid=29045] vsize: 37928
Current children cumulated CPU time (s) 429.35
Current children cumulated vsize (Kb) 40052

[startup+440.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9059 0 0 0 43878 57 0 0 25 0 1 0 1784101354 38903808 8945 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9498 8945 145 145 0 9353 0
[pid=29045] vsize: 37992
Current children cumulated CPU time (s) 439.35
Current children cumulated vsize (Kb) 40116

[startup+450.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9059 0 0 0 44878 57 0 0 25 0 1 0 1784101354 38903808 8945 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9498 8945 145 145 0 9353 0
[pid=29045] vsize: 37992
Current children cumulated CPU time (s) 449.35
Current children cumulated vsize (Kb) 40116

[startup+460.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9059 0 0 0 45878 57 0 0 25 0 1 0 1784101354 38903808 8945 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9498 8945 145 145 0 9353 0
[pid=29045] vsize: 37992
Current children cumulated CPU time (s) 459.35
Current children cumulated vsize (Kb) 40116

[startup+470.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9065 0 0 0 46878 58 0 0 25 0 1 0 1784101354 38936576 8951 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9506 8951 145 145 0 9361 0
[pid=29045] vsize: 38024
Current children cumulated CPU time (s) 469.36
Current children cumulated vsize (Kb) 40148

[startup+480.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9065 0 0 0 47879 58 0 0 25 0 1 0 1784101354 38936576 8951 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9506 8951 145 145 0 9361 0
[pid=29045] vsize: 38024
Current children cumulated CPU time (s) 479.37
Current children cumulated vsize (Kb) 40148

[startup+490.039 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9065 0 0 0 48879 58 0 0 25 0 1 0 1784101354 38936576 8951 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9506 8951 145 145 0 9361 0
[pid=29045] vsize: 38024
Current children cumulated CPU time (s) 489.37
Current children cumulated vsize (Kb) 40148

[startup+500.039 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9088 0 0 0 49879 58 0 0 25 0 1 0 1784101354 39034880 8974 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9530 8974 145 145 0 9385 0
[pid=29045] vsize: 38120
Current children cumulated CPU time (s) 499.37
Current children cumulated vsize (Kb) 40244

[startup+510.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9095 0 0 0 50879 58 0 0 25 0 1 0 1784101354 39096320 8981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9545 8981 145 145 0 9400 0
[pid=29045] vsize: 38180
Current children cumulated CPU time (s) 509.37
Current children cumulated vsize (Kb) 40304

[startup+520.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9103 0 0 0 51879 58 0 0 25 0 1 0 1784101354 39129088 8989 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9553 8989 145 145 0 9408 0
[pid=29045] vsize: 38212
Current children cumulated CPU time (s) 519.37
Current children cumulated vsize (Kb) 40336

[startup+530.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9128 0 0 0 52879 58 0 0 25 0 1 0 1784101354 39260160 9014 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9585 9014 145 145 0 9440 0
[pid=29045] vsize: 38340
Current children cumulated CPU time (s) 529.37
Current children cumulated vsize (Kb) 40464

[startup+540.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9149 0 0 0 53880 58 0 0 25 0 1 0 1784101354 39358464 9035 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9609 9035 145 145 0 9464 0
[pid=29045] vsize: 38436
Current children cumulated CPU time (s) 539.38
Current children cumulated vsize (Kb) 40560

[startup+550.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9150 0 0 0 54879 58 0 0 25 0 1 0 1784101354 39358464 9036 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9609 9036 145 145 0 9464 0
[pid=29045] vsize: 38436
Current children cumulated CPU time (s) 549.37
Current children cumulated vsize (Kb) 40560

[startup+560.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9157 0 0 0 55880 58 0 0 25 0 1 0 1784101354 39391232 9043 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9617 9043 145 145 0 9472 0
[pid=29045] vsize: 38468
Current children cumulated CPU time (s) 559.38
Current children cumulated vsize (Kb) 40592

[startup+570.044 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9198 0 0 0 56880 58 0 0 25 0 1 0 1784101354 39620608 9084 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9084 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 569.38
Current children cumulated vsize (Kb) 40816

[startup+580.044 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9199 0 0 0 57879 59 0 0 25 0 1 0 1784101354 39620608 9085 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9085 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 579.38
Current children cumulated vsize (Kb) 40816

[startup+590.045 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 58879 60 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 589.39
Current children cumulated vsize (Kb) 40816

[startup+600.046 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 59879 60 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 599.39
Current children cumulated vsize (Kb) 40816

[startup+610.046 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 60879 61 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 609.4
Current children cumulated vsize (Kb) 40816

[startup+620.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 61879 61 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 619.4
Current children cumulated vsize (Kb) 40816

[startup+630.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 62879 61 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 629.4
Current children cumulated vsize (Kb) 40816

[startup+640.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 63878 61 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 639.39
Current children cumulated vsize (Kb) 40816

[startup+650.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 64878 61 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 649.39
Current children cumulated vsize (Kb) 40816

[startup+660.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 65878 61 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 659.39
Current children cumulated vsize (Kb) 40816

[startup+670.051 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 66878 62 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 669.4
Current children cumulated vsize (Kb) 40816

[startup+680.052 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 67878 62 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 679.4
Current children cumulated vsize (Kb) 40816

[startup+690.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9200 0 0 0 68878 62 0 0 25 0 1 0 1784101354 39620608 9086 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9673 9086 145 145 0 9528 0
[pid=29045] vsize: 38692
Current children cumulated CPU time (s) 689.4
Current children cumulated vsize (Kb) 40816

[startup+700.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9224 0 0 0 69878 62 0 0 25 0 1 0 1784101354 39751680 9110 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9705 9110 145 145 0 9560 0
[pid=29045] vsize: 38820
Current children cumulated CPU time (s) 699.4
Current children cumulated vsize (Kb) 40944

[startup+710.054 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9225 0 0 0 70879 62 0 0 25 0 1 0 1784101354 39751680 9111 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9705 9111 145 145 0 9560 0
[pid=29045] vsize: 38820
Current children cumulated CPU time (s) 709.41
Current children cumulated vsize (Kb) 40944

[startup+720.055 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9227 0 0 0 71879 62 0 0 25 0 1 0 1784101354 39751680 9113 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9705 9113 145 145 0 9560 0
[pid=29045] vsize: 38820
Current children cumulated CPU time (s) 719.41
Current children cumulated vsize (Kb) 40944

[startup+730.055 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9227 0 0 0 72879 62 0 0 25 0 1 0 1784101354 39751680 9113 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9705 9113 145 145 0 9560 0
[pid=29045] vsize: 38820
Current children cumulated CPU time (s) 729.41
Current children cumulated vsize (Kb) 40944

[startup+740.056 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9228 0 0 0 73879 62 0 0 25 0 1 0 1784101354 39751680 9114 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9705 9114 145 145 0 9560 0
[pid=29045] vsize: 38820
Current children cumulated CPU time (s) 739.41
Current children cumulated vsize (Kb) 40944

[startup+750.057 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9229 0 0 0 74879 62 0 0 25 0 1 0 1784101354 39751680 9115 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9705 9115 145 145 0 9560 0
[pid=29045] vsize: 38820
Current children cumulated CPU time (s) 749.41
Current children cumulated vsize (Kb) 40944

[startup+760.058 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9229 0 0 0 75880 62 0 0 25 0 1 0 1784101354 39751680 9115 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9705 9115 145 145 0 9560 0
[pid=29045] vsize: 38820
Current children cumulated CPU time (s) 759.42
Current children cumulated vsize (Kb) 40944

[startup+770.058 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9229 0 0 0 76880 63 0 0 25 0 1 0 1784101354 39751680 9115 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9705 9115 145 145 0 9560 0
[pid=29045] vsize: 38820
Current children cumulated CPU time (s) 769.43
Current children cumulated vsize (Kb) 40944

[startup+780.059 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9244 0 0 0 77880 63 0 0 25 0 1 0 1784101354 39849984 9130 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9729 9130 145 145 0 9584 0
[pid=29045] vsize: 38916
Current children cumulated CPU time (s) 779.43
Current children cumulated vsize (Kb) 41040

[startup+790.059 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 78880 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 789.43
Current children cumulated vsize (Kb) 41104

[startup+800.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 79880 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 799.43
Current children cumulated vsize (Kb) 41104

[startup+810.061 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 80880 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 809.43
Current children cumulated vsize (Kb) 41104

[startup+820.061 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 81881 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 819.44
Current children cumulated vsize (Kb) 41104

[startup+830.062 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 82881 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223136 134554757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 829.44
Current children cumulated vsize (Kb) 41104

[startup+840.062 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 83881 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 839.44
Current children cumulated vsize (Kb) 41104

[startup+850.063 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 84881 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 849.44
Current children cumulated vsize (Kb) 41104

[startup+860.063 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 85881 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 859.44
Current children cumulated vsize (Kb) 41104

[startup+870.064 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 86881 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 869.44
Current children cumulated vsize (Kb) 41104

[startup+880.065 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9255 0 0 0 87882 63 0 0 25 0 1 0 1784101354 39915520 9141 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9141 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 879.45
Current children cumulated vsize (Kb) 41104

[startup+890.065 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9257 0 0 0 88882 63 0 0 25 0 1 0 1784101354 39915520 9143 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9143 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 889.45
Current children cumulated vsize (Kb) 41104

[startup+900.066 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9259 0 0 0 89882 63 0 0 25 0 1 0 1784101354 39915520 9145 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9145 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 899.45
Current children cumulated vsize (Kb) 41104

[startup+910.066 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9259 0 0 0 90882 63 0 0 25 0 1 0 1784101354 39915520 9145 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9145 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 909.45
Current children cumulated vsize (Kb) 41104

[startup+920.067 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9259 0 0 0 91882 64 0 0 25 0 1 0 1784101354 39915520 9145 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9145 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 919.46
Current children cumulated vsize (Kb) 41104

[startup+930.068 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9259 0 0 0 92883 64 0 0 25 0 1 0 1784101354 39915520 9145 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9145 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 929.47
Current children cumulated vsize (Kb) 41104

[startup+940.069 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9261 0 0 0 93883 64 0 0 25 0 1 0 1784101354 39915520 9147 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9745 9147 145 145 0 9600 0
[pid=29045] vsize: 38980
Current children cumulated CPU time (s) 939.47
Current children cumulated vsize (Kb) 41104

[startup+950.069 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9266 0 0 0 94883 64 0 0 25 0 1 0 1784101354 39948288 9152 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9753 9152 145 145 0 9608 0
[pid=29045] vsize: 39012
Current children cumulated CPU time (s) 949.47
Current children cumulated vsize (Kb) 41136

[startup+960.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9272 0 0 0 95883 64 0 0 25 0 1 0 1784101354 39981056 9158 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9761 9158 145 145 0 9616 0
[pid=29045] vsize: 39044
Current children cumulated CPU time (s) 959.47
Current children cumulated vsize (Kb) 41168

[startup+970.071 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9304 0 0 0 96884 64 0 0 25 0 1 0 1784101354 40177664 9190 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9809 9190 145 145 0 9664 0
[pid=29045] vsize: 39236
Current children cumulated CPU time (s) 969.48
Current children cumulated vsize (Kb) 41360

[startup+980.071 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9308 0 0 0 97884 64 0 0 25 0 1 0 1784101354 40177664 9194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9809 9194 145 145 0 9664 0
[pid=29045] vsize: 39236
Current children cumulated CPU time (s) 979.48
Current children cumulated vsize (Kb) 41360

[startup+990.072 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9309 0 0 0 98884 64 0 0 25 0 1 0 1784101354 40177664 9195 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9809 9195 145 145 0 9664 0
[pid=29045] vsize: 39236
Current children cumulated CPU time (s) 989.48
Current children cumulated vsize (Kb) 41360

[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9309 0 0 0 99884 64 0 0 25 0 1 0 1784101354 40177664 9195 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9809 9195 145 145 0 9664 0
[pid=29045] vsize: 39236
Current children cumulated CPU time (s) 999.48
Current children cumulated vsize (Kb) 41360

[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9309 0 0 0 100884 64 0 0 25 0 1 0 1784101354 40177664 9195 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9809 9195 145 145 0 9664 0
[pid=29045] vsize: 39236
Current children cumulated CPU time (s) 1009.48
Current children cumulated vsize (Kb) 41360

[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9309 0 0 0 101884 64 0 0 25 0 1 0 1784101354 40177664 9195 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9809 9195 145 145 0 9664 0
[pid=29045] vsize: 39236
Current children cumulated CPU time (s) 1019.48
Current children cumulated vsize (Kb) 41360

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9309 0 0 0 102884 64 0 0 25 0 1 0 1784101354 40177664 9195 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9809 9195 145 145 0 9664 0
[pid=29045] vsize: 39236
Current children cumulated CPU time (s) 1029.48
Current children cumulated vsize (Kb) 41360

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9309 0 0 0 103885 64 0 0 25 0 1 0 1784101354 40177664 9195 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9809 9195 145 145 0 9664 0
[pid=29045] vsize: 39236
Current children cumulated CPU time (s) 1039.49
Current children cumulated vsize (Kb) 41360

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9315 0 0 0 104885 64 0 0 25 0 1 0 1784101354 40210432 9201 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9817 9201 145 145 0 9672 0
[pid=29045] vsize: 39268
Current children cumulated CPU time (s) 1049.49
Current children cumulated vsize (Kb) 41392

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9315 0 0 0 105885 64 0 0 25 0 1 0 1784101354 40210432 9201 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9817 9201 145 145 0 9672 0
[pid=29045] vsize: 39268
Current children cumulated CPU time (s) 1059.49
Current children cumulated vsize (Kb) 41392

[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9321 0 0 0 106885 65 0 0 25 0 1 0 1784101354 40243200 9207 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9825 9207 145 145 0 9680 0
[pid=29045] vsize: 39300
Current children cumulated CPU time (s) 1069.5
Current children cumulated vsize (Kb) 41424

[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9333 0 0 0 107885 65 0 0 25 0 1 0 1784101354 40308736 9219 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9841 9219 145 145 0 9696 0
[pid=29045] vsize: 39364
Current children cumulated CPU time (s) 1079.5
Current children cumulated vsize (Kb) 41488

[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9335 0 0 0 108885 65 0 0 25 0 1 0 1784101354 40308736 9221 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9841 9221 145 145 0 9696 0
[pid=29045] vsize: 39364
Current children cumulated CPU time (s) 1089.5
Current children cumulated vsize (Kb) 41488

[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9335 0 0 0 109886 65 0 0 25 0 1 0 1784101354 40308736 9221 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9841 9221 145 145 0 9696 0
[pid=29045] vsize: 39364
Current children cumulated CPU time (s) 1099.51
Current children cumulated vsize (Kb) 41488

[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9340 0 0 0 110886 65 0 0 25 0 1 0 1784101354 40341504 9226 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9849 9226 145 145 0 9704 0
[pid=29045] vsize: 39396
Current children cumulated CPU time (s) 1109.51
Current children cumulated vsize (Kb) 41520

[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9340 0 0 0 111886 65 0 0 25 0 1 0 1784101354 40341504 9226 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9849 9226 145 145 0 9704 0
[pid=29045] vsize: 39396
Current children cumulated CPU time (s) 1119.51
Current children cumulated vsize (Kb) 41520

[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9351 0 0 0 112887 65 0 0 25 0 1 0 1784101354 40407040 9237 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9865 9237 145 145 0 9720 0
[pid=29045] vsize: 39460
Current children cumulated CPU time (s) 1129.52
Current children cumulated vsize (Kb) 41584

[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9354 0 0 0 113887 65 0 0 25 0 1 0 1784101354 40407040 9240 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9865 9240 145 145 0 9720 0
[pid=29045] vsize: 39460
Current children cumulated CPU time (s) 1139.52
Current children cumulated vsize (Kb) 41584

[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9354 0 0 0 114887 65 0 0 25 0 1 0 1784101354 40407040 9240 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9865 9240 145 145 0 9720 0
[pid=29045] vsize: 39460
Current children cumulated CPU time (s) 1149.52
Current children cumulated vsize (Kb) 41584

[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9438 0 0 0 115886 65 0 0 25 0 1 0 1784101354 40751104 9324 4294967295 134512640 135094434 3221224448 3221223040 134557398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 9949 9324 145 145 0 9804 0
[pid=29045] vsize: 39796
Current children cumulated CPU time (s) 1159.51
Current children cumulated vsize (Kb) 41920

[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9745 0 0 0 116881 67 0 0 25 0 1 0 1784101354 42012672 9631 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 10257 9631 145 145 0 10112 0
[pid=29045] vsize: 41028
Current children cumulated CPU time (s) 1169.48
Current children cumulated vsize (Kb) 43152

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 9964 0 0 0 117875 70 0 0 25 0 1 0 1784101354 42905600 9850 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 10475 9850 145 145 0 10330 0
[pid=29045] vsize: 41900
Current children cumulated CPU time (s) 1179.45
Current children cumulated vsize (Kb) 44024

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 10162 0 0 0 118871 71 0 0 25 0 1 0 1784101354 43712512 10048 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 10672 10048 145 145 0 10527 0
[pid=29045] vsize: 42688
Current children cumulated CPU time (s) 1189.42
Current children cumulated vsize (Kb) 44812

[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 10320 0 0 0 119868 73 0 0 25 0 1 0 1784101354 44666880 10206 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 10905 10206 145 145 0 10760 0
[pid=29045] vsize: 43620
Current children cumulated CPU time (s) 1199.41
Current children cumulated vsize (Kb) 45744

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 10449 0 0 0 120867 74 0 0 25 0 1 0 1784101354 45191168 10335 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 11033 10335 145 145 0 10888 0
[pid=29045] vsize: 44132
Current children cumulated CPU time (s) 1209.41
Current children cumulated vsize (Kb) 46256



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29045
Raw data (/proc/29041/stat): 29041 (minisat+_script) S 29040 29041 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784101349 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29041/statm): 531 226 485 147 0 384 0
[pid=29041] vsize: 2124
Raw data (/proc/29045/stat): 29045 (minisat+_64-bit) R 29041 29041 22582 0 -1 0 10449 0 0 0 120867 74 0 0 25 0 1 0 1784101354 45191168 10335 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29045/statm): 11033 10335 145 145 0 10888 0
[pid=29045] vsize: 44132
Current children cumulated CPU time (s) 1209.41
Current children cumulated vsize (Kb) 46256

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.43
CPU user time (s): 1208.67
CPU system time (s): 0.760884
CPU usage (%): 99.9436
Max. virtual memory (cumulated for all children) (Kb): 46256
Name	submitted/manquinho/primes-dimacs-cnf/normalized-ii32d2.opb
MD5SUM	a483fc3761bb4050329265bf3a3a7ca5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	372
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	1.09383
Number of variables	808
Total number of constraints	5557
Number of constraints which are clauses	5557
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Some explanations

General information on the benchmark

Trace number 1518

Launcher Data

Solver Data

Watcher Data

Verifier Data
