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/17086/stat): 17086 (minisat+_script) R 17085 17086 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785817119 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/17086/statm): 174 3 169 147 0 27 0
[pid=17086] 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=17087
New process pid=17088
New process pid=17089
execve syscall for /bin/sed executable
One traced child (pid=17088) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=17089) exited with status: 0
One traced child (pid=17087) exited with status: 0
New process pid=17090
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-dfl001.opb
One traced child (pid=17090) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=17091
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-dfl001.opb

[startup+10.0037 s]
Raw data (loadavg): 1.01 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 10238 0 3 0 877 52 0 0 25 0 1 0 1785817130 43626496 9241 4294967295 134512640 135167914 3221224448 3221222784 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 10651 9241 162 162 0 10489 0
[pid=17091] vsize: 42604
Current children cumulated CPU time (s) 9.32
Current children cumulated vsize (Kb) 44732

[startup+20.0045 s]
Raw data (loadavg): 1.01 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 12491 0 3 0 1852 65 0 0 25 0 1 0 1785817130 51200000 11415 4294967295 134512640 135167914 3221224448 3221222060 134695248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 12500 11415 162 162 0 12338 0
[pid=17091] vsize: 50000
Current children cumulated CPU time (s) 19.2
Current children cumulated vsize (Kb) 52128

[startup+30.0057 s]
Raw data (loadavg): 1.01 0.97 0.93 1/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 15750 0 3 0 2814 81 0 0 25 0 1 0 1785817130 62361600 14555 4294967295 134512640 135167914 3221224448 3221222572 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 15225 14555 162 162 0 15063 0
[pid=17091] vsize: 60900
Current children cumulated CPU time (s) 28.98
Current children cumulated vsize (Kb) 63028

[startup+40.0062 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 18945 0 3 0 3775 98 0 0 25 0 1 0 1785817130 92516352 17750 4294967295 134512640 135167914 3221224448 3221221744 134843074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 22587 17750 162 162 0 22425 0
[pid=17091] vsize: 90348
Current children cumulated CPU time (s) 38.76
Current children cumulated vsize (Kb) 92476

[startup+50.0071 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 22605 0 3 0 4731 119 0 0 25 0 1 0 1785817130 103723008 20712 4294967295 134512640 135167914 3221224448 3221222720 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 25323 20712 162 162 0 25161 0
[pid=17091] vsize: 101292
Current children cumulated CPU time (s) 48.53
Current children cumulated vsize (Kb) 103420

[startup+60.008 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 25741 0 3 0 5693 134 0 0 25 0 1 0 1785817130 114880512 23712 4294967295 134512640 135167914 3221224448 3221221324 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 28047 23712 162 162 0 27885 0
[pid=17091] vsize: 112188
Current children cumulated CPU time (s) 58.3
Current children cumulated vsize (Kb) 114316

[startup+70.0088 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 28757 0 3 0 6656 150 0 0 19 0 1 0 1785817130 126054400 26650 4294967295 134512640 135167914 3221224448 3221223200 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 30775 26650 162 162 0 30613 0
[pid=17091] vsize: 123100
Current children cumulated CPU time (s) 68.09
Current children cumulated vsize (Kb) 125228

[startup+80.0107 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 33030 0 3 0 7616 171 0 0 25 0 1 0 1785817130 139460608 30121 4294967295 134512640 135167914 3221224448 3221221728 134516662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 34048 30121 162 162 0 33886 0
[pid=17091] vsize: 136192
Current children cumulated CPU time (s) 77.9
Current children cumulated vsize (Kb) 138320

[startup+90.0115 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 35988 0 3 0 8577 190 0 0 25 0 1 0 1785817130 150765568 33047 4294967295 134512640 135167914 3221224448 3221223152 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 36808 33047 162 162 0 36646 0
[pid=17091] vsize: 147232
Current children cumulated CPU time (s) 87.7
Current children cumulated vsize (Kb) 149360

[startup+100.013 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 38766 0 3 0 9540 206 0 0 25 0 1 0 1785817130 161624064 35825 4294967295 134512640 135167914 3221224448 3221221972 134581188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 39459 35825 162 162 0 39297 0
[pid=17091] vsize: 157836
Current children cumulated CPU time (s) 97.49
Current children cumulated vsize (Kb) 159964

[startup+110.014 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 41498 0 3 0 10500 225 0 0 18 0 1 0 1785817130 172425216 38557 4294967295 134512640 135167914 3221224448 3221222800 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 42096 38557 162 162 0 41934 0
[pid=17091] vsize: 168384
Current children cumulated CPU time (s) 107.28
Current children cumulated vsize (Kb) 170512

[startup+120.015 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 48402 0 3 0 11441 254 0 0 25 0 1 0 1785817130 199999488 45330 4294967295 134512640 135167914 3221224448 3221223204 134697042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 48828 45330 162 162 0 48666 0
[pid=17091] vsize: 195312
Current children cumulated CPU time (s) 116.98
Current children cumulated vsize (Kb) 197440

[startup+130.016 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 48403 0 3 0 12441 254 0 0 25 0 1 0 1785817130 199999488 45331 4294967295 134512640 135167914 3221224448 3221223296 134596402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 48828 45331 162 162 0 48666 0
[pid=17091] vsize: 195312
Current children cumulated CPU time (s) 126.98
Current children cumulated vsize (Kb) 197440

[startup+140.017 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 48406 0 3 0 13441 254 0 0 25 0 1 0 1785817130 200003584 45334 4294967295 134512640 135167914 3221224448 3221223280 134595516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 48829 45334 162 162 0 48667 0
[pid=17091] vsize: 195316
Current children cumulated CPU time (s) 136.98
Current children cumulated vsize (Kb) 197444

[startup+150.019 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 48407 0 3 0 14441 254 0 0 25 0 1 0 1785817130 200003584 45335 4294967295 134512640 135167914 3221224448 3221223296 134596393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 48829 45335 162 162 0 48667 0
[pid=17091] vsize: 195316
Current children cumulated CPU time (s) 146.98
Current children cumulated vsize (Kb) 197444

[startup+160.02 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 48411 0 3 0 15442 254 0 0 25 0 1 0 1785817130 200003584 45339 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 48829 45339 162 162 0 48667 0
[pid=17091] vsize: 195316
Current children cumulated CPU time (s) 156.99
Current children cumulated vsize (Kb) 197444

[startup+170.02 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 48421 0 3 0 16442 254 0 0 25 0 1 0 1785817130 200011776 45349 4294967295 134512640 135167914 3221224448 3221223276 134691389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 48831 45349 162 162 0 48669 0
[pid=17091] vsize: 195324
Current children cumulated CPU time (s) 166.99
Current children cumulated vsize (Kb) 197452

[startup+180.021 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 48475 0 3 0 17441 255 0 0 25 0 1 0 1785817130 191344640 43254 4294967295 134512640 135167914 3221224448 3221220736 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 46715 43254 162 162 0 46553 0
[pid=17091] vsize: 186860
Current children cumulated CPU time (s) 176.99
Current children cumulated vsize (Kb) 188988

[startup+190.022 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 48486 0 3 0 18439 256 0 0 25 0 1 0 1785817130 191389696 43265 4294967295 134512640 135167914 3221224448 3221056116 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 46726 43265 162 162 0 46564 0
[pid=17091] vsize: 186904
Current children cumulated CPU time (s) 186.98
Current children cumulated vsize (Kb) 189032

[startup+200.023 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 50477 0 3 0 19424 264 0 0 25 0 1 0 1785817130 198193152 44926 4294967295 134512640 135167914 3221224448 3221061276 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 48387 44926 162 162 0 48225 0
[pid=17091] vsize: 193548
Current children cumulated CPU time (s) 196.91
Current children cumulated vsize (Kb) 195676

[startup+210.024 s]
Raw data (loadavg): 1.00 0.97 0.93 1/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 53993 0 3 0 20396 277 0 0 25 0 1 0 1785817130 209895424 47783 4294967295 134512640 135167914 3221224448 3221074588 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 51244 47783 162 162 0 51082 0
[pid=17091] vsize: 204976
Current children cumulated CPU time (s) 206.76
Current children cumulated vsize (Kb) 207104

[startup+220.025 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 56318 0 3 0 21369 286 0 0 25 0 1 0 1785817130 219418624 50108 4294967295 134512640 135167914 3221224448 3221058716 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 53569 50108 162 162 0 53407 0
[pid=17091] vsize: 214276
Current children cumulated CPU time (s) 216.58
Current children cumulated vsize (Kb) 216404

[startup+230.026 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 61050 0 3 0 22339 302 0 0 25 0 1 0 1785817130 233402368 53522 4294967295 134512640 135167914 3221224448 3221076832 134844760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 56983 53522 162 162 0 56821 0
[pid=17091] vsize: 227932
Current children cumulated CPU time (s) 226.44
Current children cumulated vsize (Kb) 230060

[startup+240.026 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 63684 0 3 0 23309 314 0 0 25 0 1 0 1785817130 244191232 56156 4294967295 134512640 135167914 3221224448 3221068896 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 59617 56156 162 162 0 59455 0
[pid=17091] vsize: 238468
Current children cumulated CPU time (s) 236.26
Current children cumulated vsize (Kb) 240596

[startup+250.027 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 66169 0 3 0 24282 325 0 0 25 0 1 0 1785817130 254369792 58641 4294967295 134512640 135167914 3221224448 3221060320 134845090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 62102 58641 162 162 0 61940 0
[pid=17091] vsize: 248408
Current children cumulated CPU time (s) 246.1
Current children cumulated vsize (Kb) 250536

[startup+260.029 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 68482 0 3 0 25255 337 0 0 25 0 1 0 1785817130 263843840 60954 4294967295 134512640 135167914 3221224448 3221093692 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 64415 60954 162 162 0 64253 0
[pid=17091] vsize: 257660
Current children cumulated CPU time (s) 255.95
Current children cumulated vsize (Kb) 259788

[startup+270.03 s]
Raw data (loadavg): 1.00 0.97 0.93 1/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 75334 0 3 0 26225 356 0 0 25 0 1 0 1785817130 281108480 65169 4294967295 134512640 135167914 3221224448 3221067068 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 68630 65169 162 162 0 68468 0
[pid=17091] vsize: 274520
Current children cumulated CPU time (s) 265.84
Current children cumulated vsize (Kb) 276648

[startup+280.031 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 77643 0 3 0 27197 369 0 0 25 0 1 0 1785817130 290566144 67478 4294967295 134512640 135167914 3221224448 3221079120 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 70939 67478 162 162 0 70777 0
[pid=17091] vsize: 283756
Current children cumulated CPU time (s) 275.69
Current children cumulated vsize (Kb) 285884

[startup+290.032 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 80072 0 3 0 28172 379 0 0 25 0 1 0 1785817130 300515328 69907 4294967295 134512640 135167914 3221224448 3221056028 134722542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 73368 69907 162 162 0 73206 0
[pid=17091] vsize: 293472
Current children cumulated CPU time (s) 285.54
Current children cumulated vsize (Kb) 295600

[startup+300.033 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 83045 0 3 0 29139 392 0 0 25 0 1 0 1785817130 312692736 72880 4294967295 134512640 135167914 3221224448 3221088400 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 76341 72880 162 162 0 76179 0
[pid=17091] vsize: 305364
Current children cumulated CPU time (s) 295.34
Current children cumulated vsize (Kb) 307492

[startup+310.034 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 85446 0 3 0 30111 404 0 0 25 0 1 0 1785817130 322527232 75281 4294967295 134512640 135167914 3221224448 3221055624 134693618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 78742 75281 162 162 0 78580 0
[pid=17091] vsize: 314968
Current children cumulated CPU time (s) 305.18
Current children cumulated vsize (Kb) 317096

[startup+320.035 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 87822 0 3 0 31085 416 0 0 25 0 1 0 1785817130 332259328 77657 4294967295 134512640 135167914 3221224448 3221058984 134847058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 81118 77657 162 162 0 80956 0
[pid=17091] vsize: 324472
Current children cumulated CPU time (s) 315.04
Current children cumulated vsize (Kb) 326600

[startup+330.037 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 90099 0 3 0 32056 428 0 0 25 0 1 0 1785817130 341585920 79934 4294967295 134512640 135167914 3221224448 3221063088 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 83395 79934 162 162 0 83233 0
[pid=17091] vsize: 333580
Current children cumulated CPU time (s) 324.87
Current children cumulated vsize (Kb) 335708

[startup+340.038 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 101903 0 3 0 33018 459 0 0 25 0 1 0 1785817130 368336896 86465 4294967295 134512640 135167914 3221224448 3221066304 134849232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 89926 86465 162 162 0 89764 0
[pid=17091] vsize: 359704
Current children cumulated CPU time (s) 334.8
Current children cumulated vsize (Kb) 361832

[startup+350.039 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 104340 0 3 0 33993 468 0 0 25 0 1 0 1785817130 378318848 88902 4294967295 134512640 135167914 3221224448 3221069436 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 92363 88902 162 162 0 92201 0
[pid=17091] vsize: 369452
Current children cumulated CPU time (s) 344.64
Current children cumulated vsize (Kb) 371580

[startup+360.04 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 106648 0 3 0 34968 479 0 0 25 0 1 0 1785817130 387772416 91210 4294967295 134512640 135167914 3221224448 3221062064 134844854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 94671 91210 162 162 0 94509 0
[pid=17091] vsize: 378684
Current children cumulated CPU time (s) 354.5
Current children cumulated vsize (Kb) 380812

[startup+370.041 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 109215 0 3 0 35940 492 0 0 25 0 1 0 1785817130 398286848 93777 4294967295 134512640 135167914 3221224448 3221057248 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 97238 93777 162 162 0 97076 0
[pid=17091] vsize: 388952
Current children cumulated CPU time (s) 364.35
Current children cumulated vsize (Kb) 391080

[startup+380.041 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 111482 0 3 0 36915 501 0 0 25 0 1 0 1785817130 407572480 96044 4294967295 134512640 135167914 3221224448 3221057600 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 99505 96044 162 162 0 99343 0
[pid=17091] vsize: 398020
Current children cumulated CPU time (s) 374.19
Current children cumulated vsize (Kb) 400148

[startup+390.042 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 113856 0 3 0 37892 511 0 0 25 0 1 0 1785817130 417296384 98418 4294967295 134512640 135167914 3221224448 3221060320 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 101879 98418 162 162 0 101717 0
[pid=17091] vsize: 407516
Current children cumulated CPU time (s) 384.06
Current children cumulated vsize (Kb) 409644

[startup+400.043 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 116558 0 3 0 38863 523 0 0 25 0 1 0 1785817130 428363776 101120 4294967295 134512640 135167914 3221224448 3221088136 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 104581 101120 162 162 0 104419 0
[pid=17091] vsize: 418324
Current children cumulated CPU time (s) 393.89
Current children cumulated vsize (Kb) 420452

[startup+410.044 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 119457 0 3 0 39831 536 0 0 25 0 1 0 1785817130 440238080 104019 4294967295 134512640 135167914 3221224448 3221062492 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 107480 104019 162 162 0 107318 0
[pid=17091] vsize: 429920
Current children cumulated CPU time (s) 403.7
Current children cumulated vsize (Kb) 432048

[startup+420.045 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 122505 0 3 0 40800 548 0 0 25 0 1 0 1785817130 452722688 107067 4294967295 134512640 135167914 3221224448 3221059888 134624545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 110528 107067 162 162 0 110366 0
[pid=17091] vsize: 442112
Current children cumulated CPU time (s) 413.51
Current children cumulated vsize (Kb) 444240

[startup+430.047 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 124817 0 3 0 41777 558 0 0 25 0 1 0 1785817130 462192640 109379 4294967295 134512640 135167914 3221224448 3221059580 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 112840 109379 162 162 0 112678 0
[pid=17091] vsize: 451360
Current children cumulated CPU time (s) 423.38
Current children cumulated vsize (Kb) 453488

[startup+440.048 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 127077 0 3 0 42750 569 0 0 25 0 1 0 1785817130 471449600 111639 4294967295 134512640 135167914 3221224448 3221080480 134844723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 115100 111639 162 162 0 114938 0
[pid=17091] vsize: 460400
Current children cumulated CPU time (s) 433.22
Current children cumulated vsize (Kb) 462528

[startup+450.048 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 129577 0 3 0 43723 580 0 0 25 0 1 0 1785817130 481689600 114139 4294967295 134512640 135167914 3221224448 3221054740 134697270 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 117600 114139 162 162 0 117438 0
[pid=17091] vsize: 470400
Current children cumulated CPU time (s) 443.06
Current children cumulated vsize (Kb) 472528

[startup+460.049 s]
Raw data (loadavg): 1.00 0.97 0.93 1/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 131911 0 3 0 44695 590 0 0 25 0 1 0 1785817130 491249664 116473 4294967295 134512640 135167914 3221224448 3221057788 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 119934 116473 162 162 0 119772 0
[pid=17091] vsize: 479736
Current children cumulated CPU time (s) 452.88
Current children cumulated vsize (Kb) 481864

[startup+470.05 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 134463 0 3 0 45665 603 0 0 25 0 1 0 1785817130 501702656 119025 4294967295 134512640 135167914 3221224448 3221069984 134695806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 122486 119025 162 162 0 122324 0
[pid=17091] vsize: 489944
Current children cumulated CPU time (s) 462.71
Current children cumulated vsize (Kb) 492072

[startup+480.051 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 156358 0 3 0 46610 654 0 0 25 0 1 0 1785817130 591384576 140920 4294967295 134512640 135167914 3221224448 3221085904 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 144381 140920 162 162 0 144219 0
[pid=17091] vsize: 577524
Current children cumulated CPU time (s) 472.67
Current children cumulated vsize (Kb) 579652

[startup+490.052 s]
Raw data (loadavg): 1.00 0.97 0.93 1/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 158291 0 3 0 47585 664 0 0 25 0 1 0 1785817130 556105728 132307 4294967295 134512640 135167914 3221224448 3221053228 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 135768 132307 162 162 0 135606 0
[pid=17091] vsize: 543072
Current children cumulated CPU time (s) 482.52
Current children cumulated vsize (Kb) 545200

[startup+500.054 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 160861 0 3 0 48554 676 0 0 25 0 1 0 1785817130 566632448 134877 4294967295 134512640 135167914 3221224448 3221096540 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 138338 134877 162 162 0 138176 0
[pid=17091] vsize: 553352
Current children cumulated CPU time (s) 492.33
Current children cumulated vsize (Kb) 555480

[startup+510.055 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 163166 0 3 0 49527 688 0 0 25 0 1 0 1785817130 576073728 137182 4294967295 134512640 135167914 3221224448 3221063112 134846907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 140643 137182 162 162 0 140481 0
[pid=17091] vsize: 562572
Current children cumulated CPU time (s) 502.18
Current children cumulated vsize (Kb) 564700

[startup+520.055 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 165589 0 3 0 50501 698 0 0 25 0 1 0 1785817130 585998336 139605 4294967295 134512640 135167914 3221224448 3221075520 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 143066 139605 162 162 0 142904 0
[pid=17091] vsize: 572264
Current children cumulated CPU time (s) 512.02
Current children cumulated vsize (Kb) 574392

[startup+530.057 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 167983 0 3 0 51474 708 0 0 25 0 1 0 1785817130 595804160 141999 4294967295 134512640 135167914 3221224448 3221073316 134624363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 145460 141999 162 162 0 145298 0
[pid=17091] vsize: 581840
Current children cumulated CPU time (s) 521.85
Current children cumulated vsize (Kb) 583968

[startup+540.058 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 170282 0 3 0 52448 719 0 0 25 0 1 0 1785817130 605220864 144298 4294967295 134512640 135167914 3221224448 3221054364 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 147759 144298 162 162 0 147597 0
[pid=17091] vsize: 591036
Current children cumulated CPU time (s) 531.7
Current children cumulated vsize (Kb) 593164

[startup+550.06 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 173022 0 3 0 53419 731 0 0 25 0 1 0 1785817130 616443904 147038 4294967295 134512640 135167914 3221224448 3221067968 134845881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 150499 147038 162 162 0 150337 0
[pid=17091] vsize: 601996
Current children cumulated CPU time (s) 541.53
Current children cumulated vsize (Kb) 604124

[startup+560.061 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 175330 0 3 0 54396 741 0 0 25 0 1 0 1785817130 625897472 149346 4294967295 134512640 135167914 3221224448 3221057376 134694389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 152807 149346 162 162 0 152645 0
[pid=17091] vsize: 611228
Current children cumulated CPU time (s) 551.4
Current children cumulated vsize (Kb) 613356

[startup+570.062 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 177827 0 3 0 55367 753 0 0 25 0 1 0 1785817130 636125184 151843 4294967295 134512640 135167914 3221224448 3221060368 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 155304 151843 162 162 0 155142 0
[pid=17091] vsize: 621216
Current children cumulated CPU time (s) 561.23
Current children cumulated vsize (Kb) 623344

[startup+580.062 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 180091 0 3 0 56342 764 0 0 25 0 1 0 1785817130 645398528 154107 4294967295 134512640 135167914 3221224448 3221063888 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 157568 154107 162 162 0 157406 0
[pid=17091] vsize: 630272
Current children cumulated CPU time (s) 571.09
Current children cumulated vsize (Kb) 632400

[startup+590.063 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 182470 0 3 0 57313 776 0 0 25 0 1 0 1785817130 655142912 156486 4294967295 134512640 135167914 3221224448 3221081564 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 159947 156486 162 162 0 159785 0
[pid=17091] vsize: 639788
Current children cumulated CPU time (s) 580.92
Current children cumulated vsize (Kb) 641916

[startup+600.065 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 185254 0 3 0 58285 789 0 0 25 0 1 0 1785817130 666546176 159270 4294967295 134512640 135167914 3221224448 3221068928 134847211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 162731 159270 162 162 0 162569 0
[pid=17091] vsize: 650924
Current children cumulated CPU time (s) 590.77
Current children cumulated vsize (Kb) 653052

[startup+610.066 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 187794 0 3 0 59255 802 0 0 25 0 1 0 1785817130 676950016 161810 4294967295 134512640 135167914 3221224448 3221068276 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17091/statm): 165271 161810 162 162 0 165109 0
[pid=17091] vsize: 661084
Current children cumulated CPU time (s) 600.6
Current children cumulated vsize (Kb) 663212

[startup+620.067 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 190102 0 3 0 60229 813 0 0 25 0 1 0 1785817130 686403584 164118 4294967295 134512640 135167914 3221224448 3221065696 134844975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 167579 164118 162 162 0 167417 0
[pid=17091] vsize: 670316
Current children cumulated CPU time (s) 610.45
Current children cumulated vsize (Kb) 672444

[startup+630.068 s]
Raw data (loadavg): 1.00 0.97 0.93 1/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 192524 0 3 0 61202 823 0 0 25 0 1 0 1785817130 696324096 166540 4294967295 134512640 135167914 3221224448 3221067420 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 170001 166540 162 162 0 169839 0
[pid=17091] vsize: 680004
Current children cumulated CPU time (s) 620.28
Current children cumulated vsize (Kb) 682132

[startup+640.069 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 195028 0 3 0 62171 837 0 0 25 0 1 0 1785817130 706580480 169044 4294967295 134512640 135167914 3221224448 3221081804 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 172505 169044 162 162 0 172343 0
[pid=17091] vsize: 690020
Current children cumulated CPU time (s) 630.11
Current children cumulated vsize (Kb) 692148

[startup+650.069 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 197458 0 3 0 63144 848 0 0 25 0 1 0 1785817130 716533760 171474 4294967295 134512640 135167914 3221224448 3221059216 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 174935 171474 162 162 0 174773 0
[pid=17091] vsize: 699740
Current children cumulated CPU time (s) 639.95
Current children cumulated vsize (Kb) 701868

[startup+660.07 s]
Raw data (loadavg): 1.00 0.97 0.93 1/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) T 17086 17086 6847 0 -1 0 199803 0 3 0 64116 859 0 0 25 0 1 0 1785817130 726138880 173819 4294967295 134512640 135167914 3221224448 3221078172 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17091/statm): 177280 173819 162 162 0 177118 0
[pid=17091] vsize: 709120
Current children cumulated CPU time (s) 649.78
Current children cumulated vsize (Kb) 711248

[startup+670.071 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 202142 0 3 0 65093 868 0 0 25 0 1 0 1785817130 735719424 176158 4294967295 134512640 135167914 3221224448 3221079624 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 179619 176158 162 162 0 179457 0
[pid=17091] vsize: 718476
Current children cumulated CPU time (s) 659.64
Current children cumulated vsize (Kb) 720604

[startup+680.072 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 204314 0 3 0 66068 877 0 0 25 0 1 0 1785817130 744615936 178330 4294967295 134512640 135167914 3221224448 3221061852 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 181791 178330 162 162 0 181629 0
[pid=17091] vsize: 727164
Current children cumulated CPU time (s) 669.48
Current children cumulated vsize (Kb) 729292

[startup+690.073 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 206731 0 3 0 67040 888 0 0 25 0 1 0 1785817130 754515968 180747 4294967295 134512640 135167914 3221224448 3221062848 134694444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 184208 180747 162 162 0 184046 0
[pid=17091] vsize: 736832
Current children cumulated CPU time (s) 679.31
Current children cumulated vsize (Kb) 738960

[startup+700.074 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 209000 0 3 0 68015 897 0 0 25 0 1 0 1785817130 763809792 183016 4294967295 134512640 135167914 3221224448 3221068196 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 186477 183016 162 162 0 186315 0
[pid=17091] vsize: 745908
Current children cumulated CPU time (s) 689.15
Current children cumulated vsize (Kb) 748036

[startup+710.075 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 211401 0 3 0 68988 909 0 0 25 0 1 0 1785817130 773644288 185417 4294967295 134512640 135167914 3221224448 3221054912 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 188878 185417 162 162 0 188716 0
[pid=17091] vsize: 755512
Current children cumulated CPU time (s) 699
Current children cumulated vsize (Kb) 757640

[startup+720.074 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 213632 0 3 0 69964 920 0 0 25 0 1 0 1785817130 782782464 187648 4294967295 134512640 135167914 3221224448 3221053328 134845056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 191109 187648 162 162 0 190947 0
[pid=17091] vsize: 764436
Current children cumulated CPU time (s) 708.87
Current children cumulated vsize (Kb) 766564

[startup+730.075 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 215965 0 3 0 70936 932 0 0 25 0 1 0 1785817130 792338432 189981 4294967295 134512640 135167914 3221224448 3221057512 134846924 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 193442 189981 162 162 0 193280 0
[pid=17091] vsize: 773768
Current children cumulated CPU time (s) 718.71
Current children cumulated vsize (Kb) 775896

[startup+740.076 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 218966 0 3 0 71904 947 0 0 25 0 1 0 1785817130 804630528 192982 4294967295 134512640 135167914 3221224448 3221106256 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 196443 192982 162 162 0 196281 0
[pid=17091] vsize: 785772
Current children cumulated CPU time (s) 728.54
Current children cumulated vsize (Kb) 787900

[startup+750.077 s]
Raw data (loadavg): 1.00 0.97 0.93 2/57 17091
Raw data (/proc/17086/stat): 17086 (minisat+_script) S 17085 17086 6847 0 -1 0 314 332 0 0 0 1 1 1 20 0 1 0 1785817119 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17086/statm): 532 234 485 147 0 385 0
[pid=17086] vsize: 2128
Raw data (/proc/17091/stat): 17091 (minisat+_bignum) R 17086 17086 6847 0 -1 0 221945 0 3 0 72873 962 0 0 25 0 1 0 1785817130 816832512 195961 4294967295 134512640 135167914 3221224448 3221087732 134522324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17091/statm): 199422 195961 162 162 0 199260 0
[pid=17091] vsize: 797688
Current children cumulated CPU time (s) 738.38
Current children cumulated vsize (Kb) 799816
One traced child (pid=17091) ended because it received signal 11 (SIGSEGV)
One traced child (pid=17086) exited with status: 139
All traced children have exited ! Game is over.

Child status: 139
Real time (s): 757.446
CPU time (s): 745.676
CPU user time (s): 735.596
CPU system time (s): 10.0795
CPU usage (%): 98.4461
Max. virtual memory (cumulated for all children) (Kb): 799816