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/3870/stat): 3870 (minisat+_script) R 3869 3870 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793758571 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3870/statm): 174 3 169 147 0 27 0
[pid=3870] 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=3871
New process pid=3872
New process pid=3873
execve syscall for /bin/sed executable
One traced child (pid=3872) 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=3873) exited with status: 0
One traced child (pid=3871) exited with status: 0
New process pid=3874
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-seymour.opb

[startup+10.0031 s]
Raw data (loadavg): 0.93 0.98 0.90 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 4399 0 0 0 959 18 0 0 25 0 1 0 1793758576 20058112 4361 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 4897 4361 145 145 0 4752 0
[pid=3874] vsize: 19588
Current children cumulated CPU time (s) 9.79
Current children cumulated vsize (Kb) 21712

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 4538 0 0 0 1956 20 0 0 25 0 1 0 1793758576 20627456 4500 4294967295 134512640 135094434 3221224432 3221223088 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 5036 4500 145 145 0 4891 0
[pid=3874] vsize: 20144
Current children cumulated CPU time (s) 19.78
Current children cumulated vsize (Kb) 22268

[startup+30.0054 s]
Raw data (loadavg): 0.95 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 4723 0 0 0 2954 21 0 0 25 0 1 0 1793758576 21397504 4685 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 5224 4685 145 145 0 5079 0
[pid=3874] vsize: 20896
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 23020

[startup+40.007 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 5054 0 0 0 3947 23 0 0 25 0 1 0 1793758576 22740992 5016 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 5552 5016 145 145 0 5407 0
[pid=3874] vsize: 22208
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 24332

[startup+50.0077 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 5400 0 0 0 4940 26 0 0 25 0 1 0 1793758576 24215552 5362 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 5912 5362 145 145 0 5767 0
[pid=3874] vsize: 23648
Current children cumulated CPU time (s) 49.68
Current children cumulated vsize (Kb) 25772

[startup+60.0073 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 5643 0 0 0 5934 29 0 0 25 0 1 0 1793758576 25186304 5605 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 6149 5605 145 145 0 6004 0
[pid=3874] vsize: 24596
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 26720

[startup+70.0079 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 5815 0 0 0 6930 31 0 0 25 0 1 0 1793758576 25878528 5777 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 6318 5777 145 145 0 6173 0
[pid=3874] vsize: 25272
Current children cumulated CPU time (s) 69.63
Current children cumulated vsize (Kb) 27396

[startup+80.0086 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 6010 0 0 0 7925 34 0 0 25 0 1 0 1793758576 26664960 5972 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 6510 5972 145 145 0 6365 0
[pid=3874] vsize: 26040
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 28164

[startup+90.0092 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 6208 0 0 0 8922 35 0 0 25 0 1 0 1793758576 27590656 6170 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 6736 6170 145 145 0 6591 0
[pid=3874] vsize: 26944
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 29068

[startup+100.01 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 6469 0 0 0 9918 37 0 0 25 0 1 0 1793758576 28643328 6431 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 6993 6431 145 145 0 6848 0
[pid=3874] vsize: 27972
Current children cumulated CPU time (s) 99.57
Current children cumulated vsize (Kb) 30096

[startup+110.01 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 6635 0 0 0 10915 38 0 0 25 0 1 0 1793758576 29319168 6597 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 7158 6597 145 145 0 7013 0
[pid=3874] vsize: 28632
Current children cumulated CPU time (s) 109.55
Current children cumulated vsize (Kb) 30756

[startup+120.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 6952 0 0 0 11909 40 0 0 25 0 1 0 1793758576 30609408 6914 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 7473 6914 145 145 0 7328 0
[pid=3874] vsize: 29892
Current children cumulated CPU time (s) 119.51
Current children cumulated vsize (Kb) 32016

[startup+130.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 7300 0 0 0 12903 44 0 0 25 0 1 0 1793758576 32014336 7262 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 7816 7262 145 145 0 7671 0
[pid=3874] vsize: 31264
Current children cumulated CPU time (s) 129.49
Current children cumulated vsize (Kb) 33388

[startup+140.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 7476 0 0 0 13900 45 0 0 25 0 1 0 1793758576 32722944 7438 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 7989 7438 145 145 0 7844 0
[pid=3874] vsize: 31956
Current children cumulated CPU time (s) 139.47
Current children cumulated vsize (Kb) 34080

[startup+150.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 7651 0 0 0 14897 47 0 0 25 0 1 0 1793758576 33427456 7613 4294967295 134512640 135094434 3221224432 3221223104 134555241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 8161 7613 145 145 0 8016 0
[pid=3874] vsize: 32644
Current children cumulated CPU time (s) 149.46
Current children cumulated vsize (Kb) 34768

[startup+160.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 7875 0 0 0 15893 48 0 0 25 0 1 0 1793758576 34336768 7837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 8383 7837 145 145 0 8238 0
[pid=3874] vsize: 33532
Current children cumulated CPU time (s) 159.43
Current children cumulated vsize (Kb) 35656

[startup+170.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 8395 0 0 0 16884 52 0 0 25 0 1 0 1793758576 36450304 8357 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 8899 8357 145 145 0 8754 0
[pid=3874] vsize: 35596
Current children cumulated CPU time (s) 169.38
Current children cumulated vsize (Kb) 37720

[startup+180.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 8901 0 0 0 17875 55 0 0 25 0 1 0 1793758576 38776832 8863 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 9467 8863 145 145 0 9322 0
[pid=3874] vsize: 37868
Current children cumulated CPU time (s) 179.32
Current children cumulated vsize (Kb) 39992

[startup+190.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 9412 0 0 0 18865 59 0 0 25 0 1 0 1793758576 40857600 9374 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 9975 9374 145 145 0 9830 0
[pid=3874] vsize: 39900
Current children cumulated CPU time (s) 189.26
Current children cumulated vsize (Kb) 42024

[startup+200.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 9881 0 0 0 19854 64 0 0 25 0 1 0 1793758576 42770432 9843 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 10442 9843 145 145 0 10297 0
[pid=3874] vsize: 41768
Current children cumulated CPU time (s) 199.2
Current children cumulated vsize (Kb) 43892

[startup+210.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 10317 0 0 0 20844 68 0 0 25 0 1 0 1793758576 44544000 10279 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 10875 10279 145 145 0 10730 0
[pid=3874] vsize: 43500
Current children cumulated CPU time (s) 209.14
Current children cumulated vsize (Kb) 45624

[startup+220.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 10637 0 0 0 21839 71 0 0 25 0 1 0 1793758576 45838336 10599 4294967295 134512640 135094434 3221224432 3221223104 134556051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 11191 10599 145 145 0 11046 0
[pid=3874] vsize: 44764
Current children cumulated CPU time (s) 219.12
Current children cumulated vsize (Kb) 46888

[startup+230.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 10828 0 0 0 22835 73 0 0 25 0 1 0 1793758576 46612480 10790 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 11380 10790 145 145 0 11235 0
[pid=3874] vsize: 45520
Current children cumulated CPU time (s) 229.1
Current children cumulated vsize (Kb) 47644

[startup+240.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 11078 0 0 0 23830 75 0 0 25 0 1 0 1793758576 47636480 11040 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 11630 11040 145 145 0 11485 0
[pid=3874] vsize: 46520
Current children cumulated CPU time (s) 239.07
Current children cumulated vsize (Kb) 48644

[startup+250.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 11369 0 0 0 24824 78 0 0 25 0 1 0 1793758576 48816128 11331 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 11918 11331 145 145 0 11773 0
[pid=3874] vsize: 47672
Current children cumulated CPU time (s) 249.04
Current children cumulated vsize (Kb) 49796

[startup+260.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 11616 0 0 0 25820 80 0 0 25 0 1 0 1793758576 49815552 11578 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 12162 11578 145 145 0 12017 0
[pid=3874] vsize: 48648
Current children cumulated CPU time (s) 259.02
Current children cumulated vsize (Kb) 50772

[startup+270.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 11951 0 0 0 26814 83 0 0 25 0 1 0 1793758576 51171328 11913 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 12493 11913 145 145 0 12348 0
[pid=3874] vsize: 49972
Current children cumulated CPU time (s) 268.99
Current children cumulated vsize (Kb) 52096

[startup+280.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 12331 0 0 0 27807 87 0 0 25 0 1 0 1793758576 52715520 12293 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 12870 12293 145 145 0 12725 0
[pid=3874] vsize: 51480
Current children cumulated CPU time (s) 278.96
Current children cumulated vsize (Kb) 53604

[startup+290.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 12776 0 0 0 28799 90 0 0 25 0 1 0 1793758576 54525952 12738 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 13312 12738 145 145 0 13167 0
[pid=3874] vsize: 53248
Current children cumulated CPU time (s) 288.91
Current children cumulated vsize (Kb) 55372

[startup+300.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 13121 0 0 0 29791 93 0 0 25 0 1 0 1793758576 55926784 13083 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 13654 13083 145 145 0 13509 0
[pid=3874] vsize: 54616
Current children cumulated CPU time (s) 298.86
Current children cumulated vsize (Kb) 56740

[startup+310.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 13371 0 0 0 30787 95 0 0 25 0 1 0 1793758576 56934400 13333 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 13900 13333 145 145 0 13755 0
[pid=3874] vsize: 55600
Current children cumulated CPU time (s) 308.84
Current children cumulated vsize (Kb) 57724

[startup+320.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 13583 0 0 0 31784 97 0 0 25 0 1 0 1793758576 57786368 13545 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 14108 13545 145 145 0 13963 0
[pid=3874] vsize: 56432
Current children cumulated CPU time (s) 318.83
Current children cumulated vsize (Kb) 58556

[startup+330.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 13811 0 0 0 32780 98 0 0 25 0 1 0 1793758576 58703872 13773 4294967295 134512640 135094434 3221224432 3221223104 134556275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 14332 13773 145 145 0 14187 0
[pid=3874] vsize: 57328
Current children cumulated CPU time (s) 328.8
Current children cumulated vsize (Kb) 59452

[startup+340.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 14004 0 0 0 33777 99 0 0 25 0 1 0 1793758576 59490304 13966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 14524 13966 145 145 0 14379 0
[pid=3874] vsize: 58096
Current children cumulated CPU time (s) 338.78
Current children cumulated vsize (Kb) 60220

[startup+350.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 14223 0 0 0 34774 100 0 0 25 0 1 0 1793758576 60395520 14185 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 14745 14185 145 145 0 14600 0
[pid=3874] vsize: 58980
Current children cumulated CPU time (s) 348.76
Current children cumulated vsize (Kb) 61104

[startup+360.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 14467 0 0 0 35769 102 0 0 25 0 1 0 1793758576 61386752 14429 4294967295 134512640 135094434 3221224432 3221223024 134557253 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 14987 14429 145 145 0 14842 0
[pid=3874] vsize: 59948
Current children cumulated CPU time (s) 358.73
Current children cumulated vsize (Kb) 62072

[startup+370.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 14871 0 0 0 36761 106 0 0 25 0 1 0 1793758576 63033344 14833 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 15389 14833 145 145 0 15244 0
[pid=3874] vsize: 61556
Current children cumulated CPU time (s) 368.69
Current children cumulated vsize (Kb) 63680

[startup+380.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 15229 0 0 0 37755 109 0 0 25 0 1 0 1793758576 64491520 15191 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 15745 15191 145 145 0 15600 0
[pid=3874] vsize: 62980
Current children cumulated CPU time (s) 378.66
Current children cumulated vsize (Kb) 65104

[startup+390.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 15493 0 0 0 38750 111 0 0 25 0 1 0 1793758576 66088960 15455 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 16135 15455 145 145 0 15990 0
[pid=3874] vsize: 64540
Current children cumulated CPU time (s) 388.63
Current children cumulated vsize (Kb) 66664

[startup+400.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 15758 0 0 0 39747 112 0 0 25 0 1 0 1793758576 67170304 15720 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 16399 15720 145 145 0 16254 0
[pid=3874] vsize: 65596
Current children cumulated CPU time (s) 398.61
Current children cumulated vsize (Kb) 67720

[startup+410.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 15991 0 0 0 40743 114 0 0 25 0 1 0 1793758576 68091904 15953 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 16624 15953 145 145 0 16479 0
[pid=3874] vsize: 66496
Current children cumulated CPU time (s) 408.59
Current children cumulated vsize (Kb) 68620

[startup+420.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16246 0 0 0 41739 115 0 0 25 0 1 0 1793758576 69132288 16208 4294967295 134512640 135094434 3221224432 3221223120 134554657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 16878 16208 145 145 0 16733 0
[pid=3874] vsize: 67512
Current children cumulated CPU time (s) 418.56
Current children cumulated vsize (Kb) 69636

[startup+430.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 42736 116 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134558659 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 428.54
Current children cumulated vsize (Kb) 70384

[startup+440.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 43736 116 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 438.54
Current children cumulated vsize (Kb) 70384

[startup+450.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 44737 116 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 448.55
Current children cumulated vsize (Kb) 70384

[startup+460.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 45737 116 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 458.55
Current children cumulated vsize (Kb) 70384

[startup+470.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 46737 116 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 468.55
Current children cumulated vsize (Kb) 70384

[startup+480.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 47737 117 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 478.56
Current children cumulated vsize (Kb) 70384

[startup+490.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 48737 117 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 488.56
Current children cumulated vsize (Kb) 70384

[startup+500.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 49738 117 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 498.57
Current children cumulated vsize (Kb) 70384

[startup+510.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 50738 117 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 508.57
Current children cumulated vsize (Kb) 70384

[startup+520.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 51738 117 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 518.57
Current children cumulated vsize (Kb) 70384

[startup+530.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 52738 117 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 528.57
Current children cumulated vsize (Kb) 70384

[startup+540.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16432 0 0 0 53739 117 0 0 25 0 1 0 1793758576 69898240 16394 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16394 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 538.58
Current children cumulated vsize (Kb) 70384

[startup+550.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16437 0 0 0 54738 117 0 0 25 0 1 0 1793758576 69898240 16399 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 17065 16399 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 548.57
Current children cumulated vsize (Kb) 70384

[startup+560.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16438 0 0 0 55737 117 0 0 25 0 1 0 1793758576 69898240 16400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16400 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 558.56
Current children cumulated vsize (Kb) 70384

[startup+570.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16439 0 0 0 56737 117 0 0 25 0 1 0 1793758576 69898240 16401 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16401 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 568.56
Current children cumulated vsize (Kb) 70384

[startup+580.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16439 0 0 0 57738 117 0 0 25 0 1 0 1793758576 69898240 16401 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16401 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 578.57
Current children cumulated vsize (Kb) 70384

[startup+590.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16439 0 0 0 58738 117 0 0 25 0 1 0 1793758576 69898240 16401 4294967295 134512640 135094434 3221224432 3221223104 134555447 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16401 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 588.57
Current children cumulated vsize (Kb) 70384

[startup+600.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 59737 118 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 598.57
Current children cumulated vsize (Kb) 70384

[startup+610.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 60737 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 608.58
Current children cumulated vsize (Kb) 70384

[startup+620.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 61737 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 618.58
Current children cumulated vsize (Kb) 70384

[startup+630.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 62737 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 628.58
Current children cumulated vsize (Kb) 70384

[startup+640.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 63737 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 638.58
Current children cumulated vsize (Kb) 70384

[startup+650.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 64737 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 648.58
Current children cumulated vsize (Kb) 70384

[startup+660.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 65738 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 658.59
Current children cumulated vsize (Kb) 70384

[startup+670.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 66738 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 668.59
Current children cumulated vsize (Kb) 70384

[startup+680.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 67738 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 678.59
Current children cumulated vsize (Kb) 70384

[startup+690.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 68738 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 688.59
Current children cumulated vsize (Kb) 70384

[startup+700.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 69738 119 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 698.59
Current children cumulated vsize (Kb) 70384

[startup+710.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 70738 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 708.6
Current children cumulated vsize (Kb) 70384

[startup+720.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 71739 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 718.61
Current children cumulated vsize (Kb) 70384

[startup+730.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 72739 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 728.61
Current children cumulated vsize (Kb) 70384

[startup+740.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 73739 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 738.61
Current children cumulated vsize (Kb) 70384

[startup+750.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 74739 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 748.61
Current children cumulated vsize (Kb) 70384

[startup+760.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 75739 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 758.61
Current children cumulated vsize (Kb) 70384

[startup+770.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 76740 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223104 134555335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 768.62
Current children cumulated vsize (Kb) 70384

[startup+780.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 77740 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 778.62
Current children cumulated vsize (Kb) 70384

[startup+790.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 78740 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 788.62
Current children cumulated vsize (Kb) 70384

[startup+800.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 79740 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 798.62
Current children cumulated vsize (Kb) 70384

[startup+810.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 80740 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 808.62
Current children cumulated vsize (Kb) 70384

[startup+820.056 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 81740 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 818.62
Current children cumulated vsize (Kb) 70384

[startup+830.056 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 82741 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 828.63
Current children cumulated vsize (Kb) 70384

[startup+840.057 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 83741 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 838.63
Current children cumulated vsize (Kb) 70384

[startup+850.058 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 84741 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 848.63
Current children cumulated vsize (Kb) 70384

[startup+860.059 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 85742 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 858.64
Current children cumulated vsize (Kb) 70384

[startup+870.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 86742 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 868.64
Current children cumulated vsize (Kb) 70384

[startup+880.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 87742 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 878.64
Current children cumulated vsize (Kb) 70384

[startup+890.062 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 88742 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 888.64
Current children cumulated vsize (Kb) 70384

[startup+900.063 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16441 0 0 0 89743 120 0 0 25 0 1 0 1793758576 69898240 16403 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17065 16403 145 145 0 16920 0
[pid=3874] vsize: 68260
Current children cumulated CPU time (s) 898.65
Current children cumulated vsize (Kb) 70384

[startup+910.063 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16462 0 0 0 90743 120 0 0 25 0 1 0 1793758576 70025216 16424 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17096 16424 145 145 0 16951 0
[pid=3874] vsize: 68384
Current children cumulated CPU time (s) 908.65
Current children cumulated vsize (Kb) 70508

[startup+920.065 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16462 0 0 0 91743 120 0 0 25 0 1 0 1793758576 70025216 16424 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17096 16424 145 145 0 16951 0
[pid=3874] vsize: 68384
Current children cumulated CPU time (s) 918.65
Current children cumulated vsize (Kb) 70508

[startup+930.065 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16462 0 0 0 92743 120 0 0 25 0 1 0 1793758576 70025216 16424 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17096 16424 145 145 0 16951 0
[pid=3874] vsize: 68384
Current children cumulated CPU time (s) 928.65
Current children cumulated vsize (Kb) 70508

[startup+940.065 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16462 0 0 0 93743 121 0 0 25 0 1 0 1793758576 70025216 16424 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17096 16424 145 145 0 16951 0
[pid=3874] vsize: 68384
Current children cumulated CPU time (s) 938.66
Current children cumulated vsize (Kb) 70508

[startup+950.066 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16462 0 0 0 94744 121 0 0 25 0 1 0 1793758576 70025216 16424 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17096 16424 145 145 0 16951 0
[pid=3874] vsize: 68384
Current children cumulated CPU time (s) 948.67
Current children cumulated vsize (Kb) 70508

[startup+960.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16465 0 0 0 95744 121 0 0 25 0 1 0 1793758576 70025216 16427 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17096 16427 145 145 0 16951 0
[pid=3874] vsize: 68384
Current children cumulated CPU time (s) 958.67
Current children cumulated vsize (Kb) 70508

[startup+970.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16489 0 0 0 96744 121 0 0 25 0 1 0 1793758576 70156288 16451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17128 16451 145 145 0 16983 0
[pid=3874] vsize: 68512
Current children cumulated CPU time (s) 968.67
Current children cumulated vsize (Kb) 70636

[startup+980.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16492 0 0 0 97744 121 0 0 25 0 1 0 1793758576 70156288 16454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17128 16454 145 145 0 16983 0
[pid=3874] vsize: 68512
Current children cumulated CPU time (s) 978.67
Current children cumulated vsize (Kb) 70636

[startup+990.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16496 0 0 0 98744 121 0 0 25 0 1 0 1793758576 70156288 16458 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3874/statm): 17128 16458 145 145 0 16983 0
[pid=3874] vsize: 68512
Current children cumulated CPU time (s) 988.67
Current children cumulated vsize (Kb) 70636

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16499 0 0 0 99744 121 0 0 25 0 1 0 1793758576 70156288 16461 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17128 16461 145 145 0 16983 0
[pid=3874] vsize: 68512
Current children cumulated CPU time (s) 998.67
Current children cumulated vsize (Kb) 70636

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16502 0 0 0 100744 121 0 0 25 0 1 0 1793758576 70156288 16464 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17128 16464 145 145 0 16983 0
[pid=3874] vsize: 68512
Current children cumulated CPU time (s) 1008.67
Current children cumulated vsize (Kb) 70636

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 16917 0 0 0 101736 124 0 0 25 0 1 0 1793758576 71852032 16879 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17542 16879 145 145 0 17397 0
[pid=3874] vsize: 70168
Current children cumulated CPU time (s) 1018.62
Current children cumulated vsize (Kb) 72292

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 17277 0 0 0 102730 127 0 0 25 0 1 0 1793758576 73318400 17239 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 17900 17239 145 145 0 17755 0
[pid=3874] vsize: 71600
Current children cumulated CPU time (s) 1028.59
Current children cumulated vsize (Kb) 73724

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 17571 0 0 0 103723 130 0 0 25 0 1 0 1793758576 74510336 17533 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 18191 17533 145 145 0 18046 0
[pid=3874] vsize: 72764
Current children cumulated CPU time (s) 1038.55
Current children cumulated vsize (Kb) 74888

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 17814 0 0 0 104720 132 0 0 25 0 1 0 1793758576 75497472 17776 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 18432 17776 145 145 0 18287 0
[pid=3874] vsize: 73728
Current children cumulated CPU time (s) 1048.54
Current children cumulated vsize (Kb) 75852

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 18144 0 0 0 105713 135 0 0 25 0 1 0 1793758576 76840960 18106 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 18760 18106 145 145 0 18615 0
[pid=3874] vsize: 75040
Current children cumulated CPU time (s) 1058.5
Current children cumulated vsize (Kb) 77164

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 18503 0 0 0 106707 137 0 0 25 0 1 0 1793758576 78303232 18465 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 19117 18465 145 145 0 18972 0
[pid=3874] vsize: 76468
Current children cumulated CPU time (s) 1068.46
Current children cumulated vsize (Kb) 78592

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) T 3870 3870 15400 0 -1 0 18834 0 0 0 107700 140 0 0 25 0 1 0 1793758576 79650816 18796 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3874/statm): 19446 18796 145 145 0 19301 0
[pid=3874] vsize: 77784
Current children cumulated CPU time (s) 1078.42
Current children cumulated vsize (Kb) 79908

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19099 0 0 0 108696 142 0 0 25 0 1 0 1793758576 80732160 19061 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 19710 19061 145 145 0 19565 0
[pid=3874] vsize: 78840
Current children cumulated CPU time (s) 1088.4
Current children cumulated vsize (Kb) 80964

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19357 0 0 0 109692 144 0 0 25 0 1 0 1793758576 81784832 19319 4294967295 134512640 135094434 3221224432 3221223104 134556394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 19967 19319 145 145 0 19822 0
[pid=3874] vsize: 79868
Current children cumulated CPU time (s) 1098.38
Current children cumulated vsize (Kb) 81992

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 110691 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223024 134556837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1108.38
Current children cumulated vsize (Kb) 82176

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 111691 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1118.38
Current children cumulated vsize (Kb) 82176

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 112691 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1128.38
Current children cumulated vsize (Kb) 82176

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 113692 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1138.39
Current children cumulated vsize (Kb) 82176

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 114692 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1148.39
Current children cumulated vsize (Kb) 82176

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 115692 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1158.39
Current children cumulated vsize (Kb) 82176

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 116692 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1168.39
Current children cumulated vsize (Kb) 82176

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 117692 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1178.39
Current children cumulated vsize (Kb) 82176

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 118693 145 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1188.4
Current children cumulated vsize (Kb) 82176

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 119692 146 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1198.4
Current children cumulated vsize (Kb) 82176

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 120692 146 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1208.4
Current children cumulated vsize (Kb) 82176



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 3874
Raw data (/proc/3870/stat): 3870 (minisat+_script) S 3869 3870 15400 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1793758571 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3870/statm): 531 226 485 147 0 384 0
[pid=3870] vsize: 2124
Raw data (/proc/3874/stat): 3874 (minisat+_64-bit) R 3870 3870 15400 0 -1 0 19403 0 0 0 120692 146 0 0 25 0 1 0 1793758576 81973248 19365 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3874/statm): 20013 19365 145 145 0 19868 0
[pid=3874] vsize: 80052
Current children cumulated CPU time (s) 1208.4
Current children cumulated vsize (Kb) 82176

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1208.43
CPU user time (s): 1206.93
CPU system time (s): 1.50477
CPU usage (%): 99.8597
Max. virtual memory (cumulated for all children) (Kb): 82176
Name	mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-seymour.opb
MD5SUM	05874b307d1504e7159d47fddfd8a0be
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	460
Optimality of the best value was proved	NO
Number of terms in the objective function	1372
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	1372
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1372
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1195.05
Number of variables	1372
Total number of constraints	6316
Number of constraints which are clauses	4944
Number of constraints which are cardinality constraints (but not clauses)	1372
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	19
Some explanations

General information on the benchmark

Trace number 4550

Launcher Data

Solver Data

Watcher Data

Verifier Data
