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/6958/stat): 6958 (minisat+_script) R 6957 6958 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783138917 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6958/statm): 174 3 169 147 0 27 0
[pid=6958] 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=6959
New process pid=6960
New process pid=6961
execve syscall for /bin/sed executable
One traced child (pid=6960) 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=6961) exited with status: 0
One traced child (pid=6959) exited with status: 0
New process pid=6962
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-test4.pi.opb

[startup+10.0042 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 8406 0 0 0 943 30 0 0 25 0 1 0 1783138922 31760384 7361 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 7754 7361 145 145 0 7609 0
[pid=6962] vsize: 31016
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 33140

[startup+20.0049 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 8436 0 0 0 1941 31 0 0 25 0 1 0 1783138922 31903744 7391 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 7789 7391 145 145 0 7644 0
[pid=6962] vsize: 31156
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 33280

[startup+30.0067 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 8464 0 0 0 2941 31 0 0 25 0 1 0 1783138922 32022528 7419 4294967295 134512640 135094434 3221224448 3221223088 134562144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 7818 7419 145 145 0 7673 0
[pid=6962] vsize: 31272
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 33396

[startup+40.0074 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 8512 0 0 0 3940 32 0 0 25 0 1 0 1783138922 32239616 7467 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 7871 7467 145 145 0 7726 0
[pid=6962] vsize: 31484
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 33608

[startup+50.0081 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 8588 0 0 0 4938 32 0 0 25 0 1 0 1783138922 32538624 7543 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 7944 7543 145 145 0 7799 0
[pid=6962] vsize: 31776
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 33900

[startup+60.0089 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 9241 0 0 0 5926 37 0 0 25 0 1 0 1783138922 35250176 8196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 8606 8196 145 145 0 8461 0
[pid=6962] vsize: 34424
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 36548

[startup+70.0096 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) T 6958 6958 824 0 -1 0 10247 0 0 0 6912 41 0 0 25 0 1 0 1783138922 39354368 9202 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6962/statm): 9608 9202 145 145 0 9463 0
[pid=6962] vsize: 38432
Current children cumulated CPU time (s) 69.55
Current children cumulated vsize (Kb) 40556

[startup+80.0104 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 10887 0 0 0 7900 47 0 0 25 0 1 0 1783138922 41959424 9842 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 10244 9842 145 145 0 10099 0
[pid=6962] vsize: 40976
Current children cumulated CPU time (s) 79.49
Current children cumulated vsize (Kb) 43100

[startup+90.0111 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 11430 0 0 0 8892 51 0 0 25 0 1 0 1783138922 44294144 10385 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 10814 10385 145 145 0 10669 0
[pid=6962] vsize: 43256
Current children cumulated CPU time (s) 89.45
Current children cumulated vsize (Kb) 45380

[startup+100.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 11969 0 0 0 9883 54 0 0 25 0 1 0 1783138922 46481408 10924 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 11348 10924 145 145 0 11203 0
[pid=6962] vsize: 45392
Current children cumulated CPU time (s) 99.39
Current children cumulated vsize (Kb) 47516

[startup+110.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 12601 0 0 0 10874 58 0 0 25 0 1 0 1783138922 49053696 11556 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 11976 11556 145 145 0 11831 0
[pid=6962] vsize: 47904
Current children cumulated CPU time (s) 109.34
Current children cumulated vsize (Kb) 50028

[startup+120.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 13140 0 0 0 11865 62 0 0 25 0 1 0 1783138922 51249152 12095 4294967295 134512640 135094434 3221224448 3221223104 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 12512 12095 145 145 0 12367 0
[pid=6962] vsize: 50048
Current children cumulated CPU time (s) 119.29
Current children cumulated vsize (Kb) 52172

[startup+130.013 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 14054 0 0 0 12850 69 0 0 25 0 1 0 1783138922 54976512 13009 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 13422 13009 145 145 0 13277 0
[pid=6962] vsize: 53688
Current children cumulated CPU time (s) 129.21
Current children cumulated vsize (Kb) 55812

[startup+140.014 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 14972 0 0 0 13837 74 0 0 25 0 1 0 1783138922 58724352 13927 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 14337 13927 145 145 0 14192 0
[pid=6962] vsize: 57348
Current children cumulated CPU time (s) 139.13
Current children cumulated vsize (Kb) 59472

[startup+150.015 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 15863 0 0 0 14823 80 0 0 25 0 1 0 1783138922 62361600 14818 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 15225 14818 145 145 0 15080 0
[pid=6962] vsize: 60900
Current children cumulated CPU time (s) 149.05
Current children cumulated vsize (Kb) 63024

[startup+160.015 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 16730 0 0 0 15810 86 0 0 25 0 1 0 1783138922 65888256 15685 4294967295 134512640 135094434 3221224448 3221223120 134555837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 16086 15685 145 145 0 15941 0
[pid=6962] vsize: 64344
Current children cumulated CPU time (s) 158.98
Current children cumulated vsize (Kb) 66468

[startup+170.016 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 17541 0 0 0 16798 92 0 0 25 0 1 0 1783138922 69451776 16496 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 16956 16496 145 145 0 16811 0
[pid=6962] vsize: 67824
Current children cumulated CPU time (s) 168.92
Current children cumulated vsize (Kb) 69948

[startup+180.018 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 18561 0 0 0 17783 97 0 0 25 0 1 0 1783138922 73609216 17516 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 17971 17516 145 145 0 17826 0
[pid=6962] vsize: 71884
Current children cumulated CPU time (s) 178.82
Current children cumulated vsize (Kb) 74008

[startup+190.019 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 19425 0 0 0 18770 102 0 0 25 0 1 0 1783138922 77127680 18380 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 18830 18380 145 145 0 18685 0
[pid=6962] vsize: 75320
Current children cumulated CPU time (s) 188.74
Current children cumulated vsize (Kb) 77444

[startup+200.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 20091 0 0 0 19756 109 0 0 25 0 1 0 1783138922 79839232 19046 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 19492 19046 145 145 0 19347 0
[pid=6962] vsize: 77968
Current children cumulated CPU time (s) 198.67
Current children cumulated vsize (Kb) 80092

[startup+210.019 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 20692 0 0 0 20746 113 0 0 25 0 1 0 1783138922 82288640 19647 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 20090 19647 145 145 0 19945 0
[pid=6962] vsize: 80360
Current children cumulated CPU time (s) 208.61
Current children cumulated vsize (Kb) 82484

[startup+220.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) T 6958 6958 824 0 -1 0 21467 0 0 0 21735 117 0 0 25 0 1 0 1783138922 85454848 20422 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6962/statm): 20863 20422 145 145 0 20718 0
[pid=6962] vsize: 83452
Current children cumulated CPU time (s) 218.54
Current children cumulated vsize (Kb) 85576

[startup+230.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 22480 0 0 0 22719 125 0 0 25 0 1 0 1783138922 89595904 21435 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 21874 21435 145 145 0 21729 0
[pid=6962] vsize: 87496
Current children cumulated CPU time (s) 228.46
Current children cumulated vsize (Kb) 89620

[startup+240.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 23283 0 0 0 23706 130 0 0 25 0 1 0 1783138922 92868608 22238 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 22673 22238 145 145 0 22528 0
[pid=6962] vsize: 90692
Current children cumulated CPU time (s) 238.38
Current children cumulated vsize (Kb) 92816

[startup+250.022 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 24300 0 0 0 24692 136 0 0 25 0 1 0 1783138922 97026048 23255 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 23688 23255 145 145 0 23543 0
[pid=6962] vsize: 94752
Current children cumulated CPU time (s) 248.3
Current children cumulated vsize (Kb) 96876

[startup+260.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 25032 0 0 0 25681 141 0 0 25 0 1 0 1783138922 100016128 23987 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 24418 23987 145 145 0 24273 0
[pid=6962] vsize: 97672
Current children cumulated CPU time (s) 258.24
Current children cumulated vsize (Kb) 99796

[startup+270.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 25899 0 0 0 26666 146 0 0 25 0 1 0 1783138922 103559168 24854 4294967295 134512640 135094434 3221224448 3221223104 134557815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 25283 24854 145 145 0 25138 0
[pid=6962] vsize: 101132
Current children cumulated CPU time (s) 268.14
Current children cumulated vsize (Kb) 103256

[startup+280.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 26765 0 0 0 27657 149 0 0 25 0 1 0 1783138922 107098112 25720 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 26147 25720 145 145 0 26002 0
[pid=6962] vsize: 104588
Current children cumulated CPU time (s) 278.08
Current children cumulated vsize (Kb) 106712

[startup+290.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 27366 0 0 0 28648 153 0 0 25 0 1 0 1783138922 109547520 26321 4294967295 134512640 135094434 3221224448 3221223040 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 26745 26321 145 145 0 26600 0
[pid=6962] vsize: 106980
Current children cumulated CPU time (s) 288.03
Current children cumulated vsize (Kb) 109104

[startup+300.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 28164 0 0 0 29637 158 0 0 25 0 1 0 1783138922 112807936 27119 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 27541 27119 145 145 0 27396 0
[pid=6962] vsize: 110164
Current children cumulated CPU time (s) 297.97
Current children cumulated vsize (Kb) 112288

[startup+310.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 28781 0 0 0 30627 161 0 0 25 0 1 0 1783138922 115322880 27736 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 28155 27736 145 145 0 28010 0
[pid=6962] vsize: 112620
Current children cumulated CPU time (s) 307.9
Current children cumulated vsize (Kb) 114744

[startup+320.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 30003 0 0 0 31613 167 0 0 25 0 1 0 1783138922 120320000 28958 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 29375 28958 145 145 0 29230 0
[pid=6962] vsize: 117500
Current children cumulated CPU time (s) 317.82
Current children cumulated vsize (Kb) 119624

[startup+330.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 30950 0 0 0 32602 172 0 0 25 0 1 0 1783138922 124190720 29905 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 30320 29905 145 145 0 30175 0
[pid=6962] vsize: 121280
Current children cumulated CPU time (s) 327.76
Current children cumulated vsize (Kb) 123404

[startup+340.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 31857 0 0 0 33590 176 0 0 25 0 1 0 1783138922 127897600 30812 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 31225 30812 145 145 0 31080 0
[pid=6962] vsize: 124900
Current children cumulated CPU time (s) 337.68
Current children cumulated vsize (Kb) 127024

[startup+350.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 33002 0 0 0 34576 182 0 0 25 0 1 0 1783138922 132579328 31957 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 32368 31957 145 145 0 32223 0
[pid=6962] vsize: 129472
Current children cumulated CPU time (s) 347.6
Current children cumulated vsize (Kb) 131596

[startup+360.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 33927 0 0 0 35565 188 0 0 25 0 1 0 1783138922 136359936 32882 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 33291 32882 145 145 0 33146 0
[pid=6962] vsize: 133164
Current children cumulated CPU time (s) 357.55
Current children cumulated vsize (Kb) 135288

[startup+370.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35139 0 0 0 36551 194 0 0 25 0 1 0 1783138922 141316096 34094 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 34501 34094 145 145 0 34356 0
[pid=6962] vsize: 138004
Current children cumulated CPU time (s) 367.47
Current children cumulated vsize (Kb) 140128

[startup+380.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35824 0 0 0 37546 197 0 0 25 0 1 0 1783138922 144117760 34779 4294967295 134512640 135094434 3221224448 3221223060 134563074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34779 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 377.45
Current children cumulated vsize (Kb) 142864

[startup+390.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35824 0 0 0 38546 197 0 0 25 0 1 0 1783138922 144117760 34779 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34779 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 387.45
Current children cumulated vsize (Kb) 142864

[startup+400.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35824 0 0 0 39546 197 0 0 25 0 1 0 1783138922 144117760 34779 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 35185 34779 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 397.45
Current children cumulated vsize (Kb) 142864

[startup+410.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35824 0 0 0 40546 197 0 0 25 0 1 0 1783138922 144117760 34779 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34779 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 407.45
Current children cumulated vsize (Kb) 142864

[startup+420.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35824 0 0 0 41546 197 0 0 25 0 1 0 1783138922 144117760 34779 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34779 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 417.45
Current children cumulated vsize (Kb) 142864

[startup+430.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35824 0 0 0 42546 197 0 0 25 0 1 0 1783138922 144117760 34779 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34779 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 427.45
Current children cumulated vsize (Kb) 142864

[startup+440.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35825 0 0 0 43546 197 0 0 25 0 1 0 1783138922 144117760 34780 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34780 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 437.45
Current children cumulated vsize (Kb) 142864

[startup+450.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35825 0 0 0 44546 197 0 0 25 0 1 0 1783138922 144117760 34780 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34780 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 447.45
Current children cumulated vsize (Kb) 142864

[startup+460.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35825 0 0 0 45547 197 0 0 25 0 1 0 1783138922 144117760 34780 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34780 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 457.46
Current children cumulated vsize (Kb) 142864

[startup+470.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35825 0 0 0 46547 197 0 0 25 0 1 0 1783138922 144117760 34780 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34780 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 467.46
Current children cumulated vsize (Kb) 142864

[startup+480.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35826 0 0 0 47547 197 0 0 25 0 1 0 1783138922 144117760 34781 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34781 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 477.46
Current children cumulated vsize (Kb) 142864

[startup+490.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 48547 197 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 487.46
Current children cumulated vsize (Kb) 142864

[startup+500.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 49548 197 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 497.47
Current children cumulated vsize (Kb) 142864

[startup+510.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 50548 197 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 507.47
Current children cumulated vsize (Kb) 142864

[startup+520.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 51548 197 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 517.47
Current children cumulated vsize (Kb) 142864

[startup+530.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 52548 197 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 527.47
Current children cumulated vsize (Kb) 142864

[startup+540.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 53549 197 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 537.48
Current children cumulated vsize (Kb) 142864

[startup+550.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 54549 198 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 547.49
Current children cumulated vsize (Kb) 142864

[startup+560.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 55548 198 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 557.48
Current children cumulated vsize (Kb) 142864

[startup+570.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 56548 198 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223120 134554886 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 567.48
Current children cumulated vsize (Kb) 142864

[startup+580.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 57548 198 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 577.48
Current children cumulated vsize (Kb) 142864

[startup+590.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 58549 198 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 587.49
Current children cumulated vsize (Kb) 142864

[startup+600.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 59549 198 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 597.49
Current children cumulated vsize (Kb) 142864

[startup+610.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 60548 199 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 607.49
Current children cumulated vsize (Kb) 142864

[startup+620.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 61548 199 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 617.49
Current children cumulated vsize (Kb) 142864

[startup+630.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 35827 0 0 0 62548 199 0 0 25 0 1 0 1783138922 144117760 34782 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 35185 34782 145 145 0 35040 0
[pid=6962] vsize: 140740
Current children cumulated CPU time (s) 627.49
Current children cumulated vsize (Kb) 142864

[startup+640.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 36716 0 0 0 63537 204 0 0 25 0 1 0 1783138922 147759104 35671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 36074 35671 145 145 0 35929 0
[pid=6962] vsize: 144296
Current children cumulated CPU time (s) 637.43
Current children cumulated vsize (Kb) 146420

[startup+650.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 37868 0 0 0 64522 210 0 0 25 0 1 0 1783138922 152477696 36823 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 37226 36823 145 145 0 37081 0
[pid=6962] vsize: 148904
Current children cumulated CPU time (s) 647.34
Current children cumulated vsize (Kb) 151028

[startup+660.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 38890 0 0 0 65509 216 0 0 25 0 1 0 1783138922 156663808 37845 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 38248 37845 145 145 0 38103 0
[pid=6962] vsize: 152992
Current children cumulated CPU time (s) 657.27
Current children cumulated vsize (Kb) 155116

[startup+670.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 39959 0 0 0 66495 222 0 0 25 0 1 0 1783138922 161042432 38914 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 39317 38914 145 145 0 39172 0
[pid=6962] vsize: 157268
Current children cumulated CPU time (s) 667.19
Current children cumulated vsize (Kb) 159392

[startup+680.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 40930 0 0 0 67485 227 0 0 25 0 1 0 1783138922 165027840 39885 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 40290 39885 145 145 0 40145 0
[pid=6962] vsize: 161160
Current children cumulated CPU time (s) 677.14
Current children cumulated vsize (Kb) 163284

[startup+690.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 41898 0 0 0 68475 231 0 0 25 0 1 0 1783138922 169000960 40853 4294967295 134512640 135094434 3221224448 3221223040 134552003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 41260 40853 145 145 0 41115 0
[pid=6962] vsize: 165040
Current children cumulated CPU time (s) 687.08
Current children cumulated vsize (Kb) 167164

[startup+700.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 42876 0 0 0 69461 237 0 0 25 0 1 0 1783138922 173015040 41831 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 42240 41831 145 145 0 42095 0
[pid=6962] vsize: 168960
Current children cumulated CPU time (s) 697
Current children cumulated vsize (Kb) 171084

[startup+710.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 43731 0 0 0 70450 241 0 0 25 0 1 0 1783138922 176541696 42686 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 43101 42686 145 145 0 42956 0
[pid=6962] vsize: 172404
Current children cumulated CPU time (s) 706.93
Current children cumulated vsize (Kb) 174528

[startup+720.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 44645 0 0 0 71440 247 0 0 25 0 1 0 1783138922 180277248 43600 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 44013 43600 145 145 0 43868 0
[pid=6962] vsize: 176052
Current children cumulated CPU time (s) 716.89
Current children cumulated vsize (Kb) 178176

[startup+730.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 45428 0 0 0 72430 251 0 0 20 0 1 0 1783138922 184016896 44383 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 44926 44383 145 145 0 44781 0
[pid=6962] vsize: 179704
Current children cumulated CPU time (s) 726.83
Current children cumulated vsize (Kb) 181828

[startup+740.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 46454 0 0 0 73416 257 0 0 25 0 1 0 1783138922 188211200 45409 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 45950 45409 145 145 0 45805 0
[pid=6962] vsize: 183800
Current children cumulated CPU time (s) 736.75
Current children cumulated vsize (Kb) 185924

[startup+750.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 47215 0 0 0 74404 261 0 0 25 0 1 0 1783138922 191315968 46170 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 46708 46170 145 145 0 46563 0
[pid=6962] vsize: 186832
Current children cumulated CPU time (s) 746.67
Current children cumulated vsize (Kb) 188956

[startup+760.059 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 47830 0 0 0 75395 266 0 0 25 0 1 0 1783138922 193822720 46785 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 47320 46785 145 145 0 47175 0
[pid=6962] vsize: 189280
Current children cumulated CPU time (s) 756.63
Current children cumulated vsize (Kb) 191404

[startup+770.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 48659 0 0 0 76382 271 0 0 25 0 1 0 1783138922 197210112 47614 4294967295 134512640 135094434 3221224448 3221223120 134555797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 48147 47614 145 145 0 48002 0
[pid=6962] vsize: 192588
Current children cumulated CPU time (s) 766.55
Current children cumulated vsize (Kb) 194712

[startup+780.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 49848 0 0 0 77366 278 0 0 25 0 1 0 1783138922 202076160 48803 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 49335 48803 145 145 0 49190 0
[pid=6962] vsize: 197340
Current children cumulated CPU time (s) 776.46
Current children cumulated vsize (Kb) 199464

[startup+790.061 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 50914 0 0 0 78353 284 0 0 25 0 1 0 1783138922 206438400 49869 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 50400 49869 145 145 0 50255 0
[pid=6962] vsize: 201600
Current children cumulated CPU time (s) 786.39
Current children cumulated vsize (Kb) 203724

[startup+800.062 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 51590 0 0 0 79344 288 0 0 25 0 1 0 1783138922 209195008 50545 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 51073 50545 145 145 0 50928 0
[pid=6962] vsize: 204292
Current children cumulated CPU time (s) 796.34
Current children cumulated vsize (Kb) 206416

[startup+810.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 52363 0 0 0 80331 293 0 0 25 0 1 0 1783138922 212357120 51318 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 51845 51318 145 145 0 51700 0
[pid=6962] vsize: 207380
Current children cumulated CPU time (s) 806.26
Current children cumulated vsize (Kb) 209504

[startup+820.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53244 0 0 0 81316 299 0 0 25 0 1 0 1783138922 215957504 52199 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 52724 52199 145 145 0 52579 0
[pid=6962] vsize: 210896
Current children cumulated CPU time (s) 816.17
Current children cumulated vsize (Kb) 213020

[startup+830.065 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 82313 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 826.16
Current children cumulated vsize (Kb) 214144

[startup+840.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 83313 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 836.16
Current children cumulated vsize (Kb) 214144

[startup+850.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 84313 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 846.16
Current children cumulated vsize (Kb) 214144

[startup+860.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 85314 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 856.17
Current children cumulated vsize (Kb) 214144

[startup+870.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 86314 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 866.17
Current children cumulated vsize (Kb) 214144

[startup+880.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 87314 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223040 134557263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 876.17
Current children cumulated vsize (Kb) 214144

[startup+890.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 88314 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 886.17
Current children cumulated vsize (Kb) 214144

[startup+900.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 89314 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 896.17
Current children cumulated vsize (Kb) 214144

[startup+910.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 90315 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 906.18
Current children cumulated vsize (Kb) 214144

[startup+920.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 91315 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223120 134555683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 916.18
Current children cumulated vsize (Kb) 214144

[startup+930.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 92315 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 926.18
Current children cumulated vsize (Kb) 214144

[startup+940.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 93315 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 936.18
Current children cumulated vsize (Kb) 214144

[startup+950.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 94314 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 946.17
Current children cumulated vsize (Kb) 214144

[startup+960.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 95315 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 956.18
Current children cumulated vsize (Kb) 214144

[startup+970.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 96315 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223120 134555846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 966.18
Current children cumulated vsize (Kb) 214144

[startup+980.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 97315 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 976.18
Current children cumulated vsize (Kb) 214144

[startup+990.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 98315 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223120 134555680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 986.18
Current children cumulated vsize (Kb) 214144

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 99316 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 996.19
Current children cumulated vsize (Kb) 214144

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 100316 301 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1006.19
Current children cumulated vsize (Kb) 214144

[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 101316 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223040 134556815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1016.2
Current children cumulated vsize (Kb) 214144

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 102316 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1026.2
Current children cumulated vsize (Kb) 214144

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 103316 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1036.2
Current children cumulated vsize (Kb) 214144

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 104317 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1046.21
Current children cumulated vsize (Kb) 214144

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 105317 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1056.21
Current children cumulated vsize (Kb) 214144

[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 106317 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223040 134557377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1066.21
Current children cumulated vsize (Kb) 214144

[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 107317 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1076.21
Current children cumulated vsize (Kb) 214144

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 108317 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1086.21
Current children cumulated vsize (Kb) 214144

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 109317 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1096.21
Current children cumulated vsize (Kb) 214144

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 110318 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1106.22
Current children cumulated vsize (Kb) 214144

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 111318 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134558129 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1116.22
Current children cumulated vsize (Kb) 214144

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 112318 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1126.22
Current children cumulated vsize (Kb) 214144

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 113318 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1136.22
Current children cumulated vsize (Kb) 214144

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 114319 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1146.23
Current children cumulated vsize (Kb) 214144

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 115319 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1156.23
Current children cumulated vsize (Kb) 214144

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 116319 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1166.23
Current children cumulated vsize (Kb) 214144

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53526 0 0 0 117319 302 0 0 25 0 1 0 1783138922 217108480 52481 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52481 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1176.23
Current children cumulated vsize (Kb) 214144

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53527 0 0 0 118320 302 0 0 25 0 1 0 1783138922 217108480 52482 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52482 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1186.24
Current children cumulated vsize (Kb) 214144

[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53527 0 0 0 119320 302 0 0 25 0 1 0 1783138922 217108480 52482 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52482 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1196.24
Current children cumulated vsize (Kb) 214144

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53527 0 0 0 120319 303 0 0 25 0 1 0 1783138922 217108480 52482 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52482 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1206.24
Current children cumulated vsize (Kb) 214144



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 6962
Raw data (/proc/6958/stat): 6958 (minisat+_script) S 6957 6958 824 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1783138917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6958/statm): 531 226 485 147 0 384 0
[pid=6958] vsize: 2124
Raw data (/proc/6962/stat): 6962 (minisat+_64-bit) R 6958 6958 824 0 -1 0 53527 0 0 0 120319 303 0 0 25 0 1 0 1783138922 217108480 52482 4294967295 134512640 135094434 3221224448 3221223040 134557372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6962/statm): 53005 52482 145 145 0 52860 0
[pid=6962] vsize: 212020
Current children cumulated CPU time (s) 1206.24
Current children cumulated vsize (Kb) 214144

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

Child status: 10
Real time (s): 1210.21
CPU time (s): 1206.34
CPU user time (s): 1203.2
CPU system time (s): 3.13452
CPU usage (%): 99.68
Max. virtual memory (cumulated for all children) (Kb): 214144