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/12407/stat): 12407 (minisat+_script) R 12406 12407 9854 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783120644 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/12407/statm): 174 3 169 147 0 27 0
[pid=12407] 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=12408
New process pid=12409
New process pid=12410
execve syscall for /bin/sed executable
One traced child (pid=12409) 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=12410) exited with status: 0
One traced child (pid=12408) exited with status: 0
New process pid=12411
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-ex5.pi.opb

[startup+10.0044 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 3224 0 0 0 969 14 0 0 25 0 1 0 1783120649 14102528 3046 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 3443 3046 145 145 0 3298 0
[pid=12411] vsize: 13772
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 15896

[startup+20.0062 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 4609 0 0 0 1948 23 0 0 25 0 1 0 1783120649 19783680 4431 4294967295 134512640 135094434 3221224448 3221223120 134556236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 4830 4431 145 145 0 4685 0
[pid=12411] vsize: 19320
Current children cumulated CPU time (s) 19.72
Current children cumulated vsize (Kb) 21444

[startup+30.0069 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 5769 0 0 0 2931 31 0 0 25 0 1 0 1783120649 24576000 5591 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 6000 5591 145 145 0 5855 0
[pid=12411] vsize: 24000
Current children cumulated CPU time (s) 29.63
Current children cumulated vsize (Kb) 26124

[startup+40.0077 s]
Raw data (loadavg): 0.95 0.97 0.91 1/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) T 12407 12407 9854 0 -1 0 6863 0 0 0 3914 38 0 0 25 0 1 0 1783120649 29036544 6685 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12411/statm): 7089 6685 145 145 0 6944 0
[pid=12411] vsize: 28356
Current children cumulated CPU time (s) 39.53
Current children cumulated vsize (Kb) 30480

[startup+50.0085 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 7912 0 0 0 4897 45 0 0 25 0 1 0 1783120649 33316864 7734 4294967295 134512640 135094434 3221224448 3221223120 134556268 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 8134 7734 145 145 0 7989 0
[pid=12411] vsize: 32536
Current children cumulated CPU time (s) 49.43
Current children cumulated vsize (Kb) 34660

[startup+60.0093 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 8966 0 0 0 5878 53 0 0 25 0 1 0 1783120649 37621760 8788 4294967295 134512640 135094434 3221224448 3221223040 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 9185 8788 145 145 0 9040 0
[pid=12411] vsize: 36740
Current children cumulated CPU time (s) 59.32
Current children cumulated vsize (Kb) 38864

[startup+70.0101 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 9822 0 0 0 6864 60 0 0 25 0 1 0 1783120649 41250816 9644 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 10071 9644 145 145 0 9926 0
[pid=12411] vsize: 40284
Current children cumulated CPU time (s) 69.25
Current children cumulated vsize (Kb) 42408

[startup+80.0109 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 10692 0 0 0 7847 67 0 0 25 0 1 0 1783120649 44802048 10514 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 10938 10514 145 145 0 10793 0
[pid=12411] vsize: 43752
Current children cumulated CPU time (s) 79.15
Current children cumulated vsize (Kb) 45876

[startup+90.0117 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 10745 0 0 0 8846 68 0 0 25 0 1 0 1783120649 45015040 10567 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 10990 10567 145 145 0 10845 0
[pid=12411] vsize: 43960
Current children cumulated CPU time (s) 89.15
Current children cumulated vsize (Kb) 46084

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 10745 0 0 0 9847 68 0 0 25 0 1 0 1783120649 45015040 10567 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 10990 10567 145 145 0 10845 0
[pid=12411] vsize: 43960
Current children cumulated CPU time (s) 99.16
Current children cumulated vsize (Kb) 46084

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 10745 0 0 0 10847 68 0 0 25 0 1 0 1783120649 45015040 10567 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 10990 10567 145 145 0 10845 0
[pid=12411] vsize: 43960
Current children cumulated CPU time (s) 109.16
Current children cumulated vsize (Kb) 46084

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 10745 0 0 0 11847 68 0 0 25 0 1 0 1783120649 45015040 10567 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 10990 10567 145 145 0 10845 0
[pid=12411] vsize: 43960
Current children cumulated CPU time (s) 119.16
Current children cumulated vsize (Kb) 46084

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 11629 0 0 0 12831 75 0 0 25 0 1 0 1783120649 48627712 11451 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 11872 11451 145 145 0 11727 0
[pid=12411] vsize: 47488
Current children cumulated CPU time (s) 129.07
Current children cumulated vsize (Kb) 49612

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12491 0 0 0 13816 81 0 0 25 0 1 0 1783120649 52150272 12313 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 12732 12313 145 145 0 12587 0
[pid=12411] vsize: 50928
Current children cumulated CPU time (s) 138.98
Current children cumulated vsize (Kb) 53052

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 14810 83 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223040 134557423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 148.94
Current children cumulated vsize (Kb) 53916

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 15810 83 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 158.94
Current children cumulated vsize (Kb) 53916

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 16810 83 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 168.94
Current children cumulated vsize (Kb) 53916

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 17811 83 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 178.95
Current children cumulated vsize (Kb) 53916

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 18810 84 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 188.95
Current children cumulated vsize (Kb) 53916

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 19810 85 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 198.96
Current children cumulated vsize (Kb) 53916

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 20809 85 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 208.95
Current children cumulated vsize (Kb) 53916

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 21809 85 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 218.95
Current children cumulated vsize (Kb) 53916

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 12708 0 0 0 22808 85 0 0 25 0 1 0 1783120649 53035008 12530 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 12948 12530 145 145 0 12803 0
[pid=12411] vsize: 51792
Current children cumulated CPU time (s) 228.94
Current children cumulated vsize (Kb) 53916

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 13332 0 0 0 23796 91 0 0 25 0 1 0 1783120649 55595008 13154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 13573 13154 145 145 0 13428 0
[pid=12411] vsize: 54292
Current children cumulated CPU time (s) 238.88
Current children cumulated vsize (Kb) 56416

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 13902 0 0 0 24789 94 0 0 25 0 1 0 1783120649 57933824 13724 4294967295 134512640 135094434 3221224448 3221223120 134556468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 14144 13724 145 145 0 13999 0
[pid=12411] vsize: 56576
Current children cumulated CPU time (s) 248.84
Current children cumulated vsize (Kb) 58700

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 14589 0 0 0 25777 99 0 0 25 0 1 0 1783120649 60747776 14411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 14831 14411 145 145 0 14686 0
[pid=12411] vsize: 59324
Current children cumulated CPU time (s) 258.77
Current children cumulated vsize (Kb) 61448

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15340 0 0 0 26763 104 0 0 25 0 1 0 1783120649 63807488 15162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15578 15162 145 145 0 15433 0
[pid=12411] vsize: 62312
Current children cumulated CPU time (s) 268.68
Current children cumulated vsize (Kb) 64436

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 27760 106 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223040 134556793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 278.67
Current children cumulated vsize (Kb) 65204

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 28760 106 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 288.67
Current children cumulated vsize (Kb) 65204

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 29760 106 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 298.67
Current children cumulated vsize (Kb) 65204

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 30760 106 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 308.67
Current children cumulated vsize (Kb) 65204

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 31761 106 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 318.68
Current children cumulated vsize (Kb) 65204

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 32760 107 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 328.68
Current children cumulated vsize (Kb) 65204

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 33761 107 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 338.69
Current children cumulated vsize (Kb) 65204

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 34761 107 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 348.69
Current children cumulated vsize (Kb) 65204

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 35761 107 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 358.69
Current children cumulated vsize (Kb) 65204

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 36761 107 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 368.69
Current children cumulated vsize (Kb) 65204

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15533 0 0 0 37761 107 0 0 25 0 1 0 1783120649 64593920 15355 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 15770 15355 145 145 0 15625 0
[pid=12411] vsize: 63080
Current children cumulated CPU time (s) 378.69
Current children cumulated vsize (Kb) 65204

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 15862 0 0 0 38754 110 0 0 25 0 1 0 1783120649 65945600 15684 4294967295 134512640 135094434 3221224448 3221223092 134562166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 16100 15684 145 145 0 15955 0
[pid=12411] vsize: 64400
Current children cumulated CPU time (s) 388.65
Current children cumulated vsize (Kb) 66524

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 16510 0 0 0 39743 114 0 0 25 0 1 0 1783120649 68599808 16332 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 16748 16332 145 145 0 16603 0
[pid=12411] vsize: 66992
Current children cumulated CPU time (s) 398.58
Current children cumulated vsize (Kb) 69116

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 17347 0 0 0 40730 120 0 0 25 0 1 0 1783120649 72028160 17169 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 17585 17169 145 145 0 17440 0
[pid=12411] vsize: 70340
Current children cumulated CPU time (s) 408.51
Current children cumulated vsize (Kb) 72464

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 17950 0 0 0 41720 124 0 0 25 0 1 0 1783120649 74489856 17772 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 18186 17772 145 145 0 18041 0
[pid=12411] vsize: 72744
Current children cumulated CPU time (s) 418.45
Current children cumulated vsize (Kb) 74868

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18523 0 0 0 42710 128 0 0 25 0 1 0 1783120649 76832768 18345 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18758 18345 145 145 0 18613 0
[pid=12411] vsize: 75032
Current children cumulated CPU time (s) 428.39
Current children cumulated vsize (Kb) 77156

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18538 0 0 0 43710 128 0 0 25 0 1 0 1783120649 76894208 18360 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18360 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 438.39
Current children cumulated vsize (Kb) 77216

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18538 0 0 0 44710 128 0 0 25 0 1 0 1783120649 76894208 18360 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18360 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 448.39
Current children cumulated vsize (Kb) 77216

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 45710 128 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223040 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 458.39
Current children cumulated vsize (Kb) 77216

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 46710 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 468.4
Current children cumulated vsize (Kb) 77216

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 47711 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 478.41
Current children cumulated vsize (Kb) 77216

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 48711 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223120 134556401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 488.41
Current children cumulated vsize (Kb) 77216

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 49711 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 498.41
Current children cumulated vsize (Kb) 77216

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 50711 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 508.41
Current children cumulated vsize (Kb) 77216

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 51712 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 518.42
Current children cumulated vsize (Kb) 77216

[startup+530.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 52711 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 528.41
Current children cumulated vsize (Kb) 77216

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 53712 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 538.42
Current children cumulated vsize (Kb) 77216

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 54712 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 548.42
Current children cumulated vsize (Kb) 77216

[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 55712 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 558.42
Current children cumulated vsize (Kb) 77216

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 56712 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 568.42
Current children cumulated vsize (Kb) 77216

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18539 0 0 0 57713 129 0 0 25 0 1 0 1783120649 76894208 18361 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18773 18361 145 145 0 18628 0
[pid=12411] vsize: 75092
Current children cumulated CPU time (s) 578.43
Current children cumulated vsize (Kb) 77216

[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 18694 0 0 0 58710 130 0 0 25 0 1 0 1783120649 77533184 18516 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 18929 18516 145 145 0 18784 0
[pid=12411] vsize: 75716
Current children cumulated CPU time (s) 588.41
Current children cumulated vsize (Kb) 77840

[startup+600.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19201 0 0 0 59700 135 0 0 25 0 1 0 1783120649 79609856 19023 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19436 19023 145 145 0 19291 0
[pid=12411] vsize: 77744
Current children cumulated CPU time (s) 598.36
Current children cumulated vsize (Kb) 79868

[startup+610.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 60691 139 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 608.31
Current children cumulated vsize (Kb) 81884

[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 61691 139 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 618.31
Current children cumulated vsize (Kb) 81884

[startup+630.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 62691 139 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 628.31
Current children cumulated vsize (Kb) 81884

[startup+640.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 63692 139 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 638.32
Current children cumulated vsize (Kb) 81884

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 64692 139 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 648.32
Current children cumulated vsize (Kb) 81884

[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 65692 139 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 658.32
Current children cumulated vsize (Kb) 81884

[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 66692 139 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 668.32
Current children cumulated vsize (Kb) 81884

[startup+680.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 67692 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 678.33
Current children cumulated vsize (Kb) 81884

[startup+690.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 68692 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 688.33
Current children cumulated vsize (Kb) 81884

[startup+700.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 69693 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 698.34
Current children cumulated vsize (Kb) 81884

[startup+710.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 70692 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 708.33
Current children cumulated vsize (Kb) 81884

[startup+720.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 71693 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 718.34
Current children cumulated vsize (Kb) 81884

[startup+730.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 72693 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 728.34
Current children cumulated vsize (Kb) 81884

[startup+740.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 73693 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 738.34
Current children cumulated vsize (Kb) 81884

[startup+750.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 74693 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 748.34
Current children cumulated vsize (Kb) 81884

[startup+760.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 75693 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 758.34
Current children cumulated vsize (Kb) 81884

[startup+770.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19705 0 0 0 76693 140 0 0 25 0 1 0 1783120649 81674240 19527 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 19940 19527 145 145 0 19795 0
[pid=12411] vsize: 79760
Current children cumulated CPU time (s) 768.34
Current children cumulated vsize (Kb) 81884

[startup+780.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 19890 0 0 0 77691 141 0 0 25 0 1 0 1783120649 82427904 19712 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 20124 19712 145 145 0 19979 0
[pid=12411] vsize: 80496
Current children cumulated CPU time (s) 778.33
Current children cumulated vsize (Kb) 82620

[startup+790.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 20504 0 0 0 78679 148 0 0 25 0 1 0 1783120649 84942848 20326 4294967295 134512640 135094434 3221224448 3221223088 134562225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 20738 20326 145 145 0 20593 0
[pid=12411] vsize: 82952
Current children cumulated CPU time (s) 788.28
Current children cumulated vsize (Kb) 85076

[startup+800.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 20989 0 0 0 79670 152 0 0 25 0 1 0 1783120649 86921216 20811 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21221 20811 145 145 0 21076 0
[pid=12411] vsize: 84884
Current children cumulated CPU time (s) 798.23
Current children cumulated vsize (Kb) 87008

[startup+810.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21523 0 0 0 80661 156 0 0 25 0 1 0 1783120649 89104384 21345 4294967295 134512640 135094434 3221224448 3221222752 134562807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21345 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 808.18
Current children cumulated vsize (Kb) 89140

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21523 0 0 0 81661 157 0 0 25 0 1 0 1783120649 89104384 21345 4294967295 134512640 135094434 3221224448 3221223120 134556478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21345 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 818.19
Current children cumulated vsize (Kb) 89140

[startup+830.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21524 0 0 0 82661 157 0 0 25 0 1 0 1783120649 89104384 21346 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21346 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 828.19
Current children cumulated vsize (Kb) 89140

[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21524 0 0 0 83661 157 0 0 25 0 1 0 1783120649 89104384 21346 4294967295 134512640 135094434 3221224448 3221223104 134557934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21346 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 838.19
Current children cumulated vsize (Kb) 89140

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21524 0 0 0 84661 157 0 0 25 0 1 0 1783120649 89104384 21346 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21346 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 848.19
Current children cumulated vsize (Kb) 89140

[startup+860.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21524 0 0 0 85661 157 0 0 25 0 1 0 1783120649 89104384 21346 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21346 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 858.19
Current children cumulated vsize (Kb) 89140

[startup+870.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21524 0 0 0 86661 158 0 0 25 0 1 0 1783120649 89104384 21346 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21346 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 868.2
Current children cumulated vsize (Kb) 89140

[startup+880.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21525 0 0 0 87661 158 0 0 25 0 1 0 1783120649 89104384 21347 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21347 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 878.2
Current children cumulated vsize (Kb) 89140

[startup+890.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21525 0 0 0 88661 158 0 0 25 0 1 0 1783120649 89104384 21347 4294967295 134512640 135094434 3221224448 3221223060 134563118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21347 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 888.2
Current children cumulated vsize (Kb) 89140

[startup+900.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21525 0 0 0 89661 158 0 0 25 0 1 0 1783120649 89104384 21347 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21347 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 898.2
Current children cumulated vsize (Kb) 89140

[startup+910.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21525 0 0 0 90661 158 0 0 25 0 1 0 1783120649 89104384 21347 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21347 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 908.2
Current children cumulated vsize (Kb) 89140

[startup+920.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21525 0 0 0 91662 158 0 0 25 0 1 0 1783120649 89104384 21347 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21347 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 918.21
Current children cumulated vsize (Kb) 89140

[startup+930.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21525 0 0 0 92662 158 0 0 25 0 1 0 1783120649 89104384 21347 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21347 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 928.21
Current children cumulated vsize (Kb) 89140

[startup+940.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21525 0 0 0 93662 158 0 0 25 0 1 0 1783120649 89104384 21347 4294967295 134512640 135094434 3221224448 3221223040 134556870 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21347 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 938.21
Current children cumulated vsize (Kb) 89140

[startup+950.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21525 0 0 0 94662 158 0 0 25 0 1 0 1783120649 89104384 21347 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21754 21347 145 145 0 21609 0
[pid=12411] vsize: 87016
Current children cumulated CPU time (s) 948.21
Current children cumulated vsize (Kb) 89140

[startup+960.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 21692 0 0 0 95660 159 0 0 25 0 1 0 1783120649 89792512 21514 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 21922 21514 145 145 0 21777 0
[pid=12411] vsize: 87688
Current children cumulated CPU time (s) 958.2
Current children cumulated vsize (Kb) 89812

[startup+970.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 22379 0 0 0 96649 164 0 0 25 0 1 0 1783120649 92622848 22201 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 22613 22201 145 145 0 22468 0
[pid=12411] vsize: 90452
Current children cumulated CPU time (s) 968.14
Current children cumulated vsize (Kb) 92576

[startup+980.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23050 0 0 0 97639 167 0 0 25 0 1 0 1783120649 95412224 22872 4294967295 134512640 135094434 3221224448 3221223104 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23294 22872 145 145 0 23149 0
[pid=12411] vsize: 93176
Current children cumulated CPU time (s) 978.07
Current children cumulated vsize (Kb) 95300

[startup+990.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 98629 171 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 988.01
Current children cumulated vsize (Kb) 97500

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 99629 171 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221222912 134780857 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 998.01
Current children cumulated vsize (Kb) 97500

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 100630 171 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223040 134557302 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1008.02
Current children cumulated vsize (Kb) 97500

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 101629 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1018.02
Current children cumulated vsize (Kb) 97500

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 102630 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134557978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1028.03
Current children cumulated vsize (Kb) 97500

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 103630 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1038.03
Current children cumulated vsize (Kb) 97500

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 104630 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1048.03
Current children cumulated vsize (Kb) 97500

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 105630 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223040 134557345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1058.03
Current children cumulated vsize (Kb) 97500

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 106630 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1068.03
Current children cumulated vsize (Kb) 97500

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 107631 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1078.04
Current children cumulated vsize (Kb) 97500

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 108631 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1088.04
Current children cumulated vsize (Kb) 97500

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 109631 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1098.04
Current children cumulated vsize (Kb) 97500

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 110631 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223120 134555676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1108.04
Current children cumulated vsize (Kb) 97500

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 111631 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1118.04
Current children cumulated vsize (Kb) 97500

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 112631 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223040 134552003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1128.04
Current children cumulated vsize (Kb) 97500

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23597 0 0 0 113631 172 0 0 25 0 1 0 1783120649 97665024 23419 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23419 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1138.04
Current children cumulated vsize (Kb) 97500

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23598 0 0 0 114632 172 0 0 25 0 1 0 1783120649 97665024 23420 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23420 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1148.05
Current children cumulated vsize (Kb) 97500

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23599 0 0 0 115632 172 0 0 25 0 1 0 1783120649 97665024 23421 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23421 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1158.05
Current children cumulated vsize (Kb) 97500

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23601 0 0 0 116632 172 0 0 25 0 1 0 1783120649 97665024 23423 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 23844 23423 145 145 0 23699 0
[pid=12411] vsize: 95376
Current children cumulated CPU time (s) 1168.05
Current children cumulated vsize (Kb) 97500

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 23973 0 0 0 117625 175 0 0 25 0 1 0 1783120649 99475456 23795 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 24286 23795 145 145 0 24141 0
[pid=12411] vsize: 97144
Current children cumulated CPU time (s) 1178.01
Current children cumulated vsize (Kb) 99268

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 24211 0 0 0 118622 177 0 0 25 0 1 0 1783120649 100450304 24033 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 24524 24033 145 145 0 24379 0
[pid=12411] vsize: 98096
Current children cumulated CPU time (s) 1188
Current children cumulated vsize (Kb) 100220

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 24211 0 0 0 119622 177 0 0 25 0 1 0 1783120649 100450304 24033 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 24524 24033 145 145 0 24379 0
[pid=12411] vsize: 98096
Current children cumulated CPU time (s) 1198
Current children cumulated vsize (Kb) 100220

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 24212 0 0 0 120623 177 0 0 25 0 1 0 1783120649 100450304 24034 4294967295 134512640 135094434 3221224448 3221223040 134557251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 24524 24034 145 145 0 24379 0
[pid=12411] vsize: 98096
Current children cumulated CPU time (s) 1208.01
Current children cumulated vsize (Kb) 100220



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12411
Raw data (/proc/12407/stat): 12407 (minisat+_script) S 12406 12407 9854 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1783120644 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12407/statm): 531 226 485 147 0 384 0
[pid=12407] vsize: 2124
Raw data (/proc/12411/stat): 12411 (minisat+_64-bit) R 12407 12407 9854 0 -1 0 24212 0 0 0 120623 177 0 0 25 0 1 0 1783120649 100450304 24034 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12411/statm): 24524 24034 145 145 0 24379 0
[pid=12411] vsize: 98096
Current children cumulated CPU time (s) 1208.01
Current children cumulated vsize (Kb) 100220

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1208.06
CPU user time (s): 1206.24
CPU system time (s): 1.82272
CPU usage (%): 99.8271
Max. virtual memory (cumulated for all children) (Kb): 100220
Name	submitted/manquinho/logic-synthesis/normalized-ex5.pi.opb
MD5SUM	ebc55cfc194a279163f52418008eccf2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	70
Optimality of the best value was proved	NO
Number of terms in the objective function	2460
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	2460
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2460
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1195.14
Number of variables	2459
Total number of constraints	873
Number of constraints which are clauses	873
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	146
Some explanations

General information on the benchmark

Trace number 910

Launcher Data

Solver Data

Watcher Data

Verifier Data
