Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namesubmitted/manquinho/primes-dimacs-cnf/normalized-f1000.opb
MD5SUM3b740c03d309134e8e181ea08fc4a1e3
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 2000
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 2000
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 2000
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2000
Total number of constraints5250
Number of constraints which are clauses5250
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint3

Trace number 1459

Launcher Data

LAUNCH ON wulflinc9 THE 2005-09-18 15:08:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2466 boxname=wulflinc9 idbench=122 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3b740c03d309134e8e181ea08fc4a1e3  /oldhome/oroussel/tmp/wulflinc9/normalized-f1000.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-f1000.opb
IDLAUNCH: 2466
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        932432 kB
Buffers:         27164 kB
Cached:          48632 kB
SwapCached:       1044 kB
Active:          29032 kB
Inactive:        49480 kB
HighTotal:      131008 kB
HighFree:        78792 kB
LowTotal:       903652 kB
LowFree:        853640 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            17920 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 15:28:56 (client local time) WITH STATUS 0 IN 1200 SECONDS
stats: 2466 7 1200 0

Solver Data

c Parsing PB file...
c Converting 5250 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5250    14750 |    1750       0        0     nan |  0.000 % |
c |       100 |    5250    14750 |    1925     100     3875    38.8 |  0.000 % |
c |       250 |    5250    14750 |    2117     250    10126    40.5 |  0.000 % |
c |       475 |    5250    14750 |    2329     475    18401    38.7 |  0.000 % |
c |       813 |    5250    14750 |    2562     813    31625    38.9 |  0.000 % |
c |      1319 |    5250    14750 |    2818    1319    51895    39.3 |  0.000 % |
c |      2079 |    5250    14750 |    3100    2079    83376    40.1 |  0.000 % |
c |      3219 |    5250    14750 |    3410    3219   133390    41.4 |  0.000 % |
c |      4927 |    5250    14750 |    3751    3134   136512    43.6 |  0.000 % |
c |      7489 |    5250    14750 |    4126    3713   163080    43.9 |  0.000 % |
c |     11335 |    5250    14750 |    4539    3280   139769    42.6 |  0.000 % |
c |     17102 |    5250    14750 |    4992    4323   194018    44.9 |  0.000 % |
c |     25751 |    5250    14750 |    5492    2626   104281    39.7 |  0.000 % |
c |     38725 |    5250    14750 |    6041    4250   177931    41.9 |  0.000 % |
c |     58186 |    5250    14750 |    6645    5028   218270    43.4 |  0.000 % |
c |     87378 |    5250    14750 |    7310    3492   135818    38.9 |  0.000 % |
c |    131170 |    5250    14750 |    8041    6015   241026    40.1 |  0.000 % |
c |    196855 |    5250    14750 |    8845    5979   238890    40.0 |  0.000 % |
c |    295382 |    5250    14750 |    9729    5160   195623    37.9 |  0.000 % |
c |    443172 |    5250    14750 |   10702    9137   375254    41.1 |  0.000 % |
c |    664860 |    5250    14750 |   11773    8065   328188    40.7 |  0.000 % |
c |    997386 |    5250    14750 |   12950    6081   232085    38.2 |  0.000 % |
c |   1496176 |    5250    14750 |   14245   12487   501590    40.2 |  0.000 % |

Watcher Data

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/4665/stat): 4665 (minisat+_script) R 4664 4665 30740 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1783991739 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/4665/statm): 174 3 169 147 0 27 0
[pid=4665] 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=4666
New process pid=4667
New process pid=4668
execve syscall for /bin/sed executable
One traced child (pid=4667) 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=4668) exited with status: 0
One traced child (pid=4666) exited with status: 0
New process pid=4669
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-f1000.opb

[startup+10.0031 s]
Raw data (loadavg): 0.39 0.61 0.82 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 655 0 0 0 989 2 0 0 25 0 1 0 1783991744 2949120 642 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 720 642 145 145 0 575 0
[pid=4669] vsize: 2880
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 5004

[startup+20.0048 s]
Raw data (loadavg): 0.49 0.62 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 741 0 0 0 1987 4 0 0 25 0 1 0 1783991744 3301376 728 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 806 728 145 145 0 661 0
[pid=4669] vsize: 3224
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 5348

[startup+30.0056 s]
Raw data (loadavg): 0.57 0.64 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 814 0 0 0 2986 4 0 0 25 0 1 0 1783991744 3600384 801 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 879 801 145 145 0 734 0
[pid=4669] vsize: 3516
Current children cumulated CPU time (s) 29.91
Current children cumulated vsize (Kb) 5640

[startup+40.0064 s]
Raw data (loadavg): 0.63 0.65 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 881 0 0 0 3984 5 0 0 25 0 1 0 1783991744 3874816 868 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 946 868 145 145 0 801 0
[pid=4669] vsize: 3784
Current children cumulated CPU time (s) 39.9
Current children cumulated vsize (Kb) 5908

[startup+50.0081 s]
Raw data (loadavg): 0.69 0.66 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 931 0 0 0 4983 6 0 0 25 0 1 0 1783991744 4079616 918 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 996 918 145 145 0 851 0
[pid=4669] vsize: 3984
Current children cumulated CPU time (s) 49.9
Current children cumulated vsize (Kb) 6108

[startup+60.0089 s]
Raw data (loadavg): 0.74 0.67 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 970 0 0 0 5982 7 0 0 25 0 1 0 1783991744 4239360 957 4294967295 134512640 135094434 3221224448 3221223040 134551914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1035 957 145 145 0 890 0
[pid=4669] vsize: 4140
Current children cumulated CPU time (s) 59.9
Current children cumulated vsize (Kb) 6264

[startup+70.0107 s]
Raw data (loadavg): 0.78 0.68 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 977 0 0 0 6982 7 0 0 25 0 1 0 1783991744 4268032 964 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1042 964 145 145 0 897 0
[pid=4669] vsize: 4168
Current children cumulated CPU time (s) 69.9
Current children cumulated vsize (Kb) 6292

[startup+80.0124 s]
Raw data (loadavg): 0.81 0.69 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1035 0 0 0 7981 8 0 0 25 0 1 0 1783991744 4534272 1022 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1107 1022 145 145 0 962 0
[pid=4669] vsize: 4428
Current children cumulated CPU time (s) 79.9
Current children cumulated vsize (Kb) 6552

[startup+90.0132 s]
Raw data (loadavg): 0.84 0.70 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1064 0 0 0 8981 8 0 0 25 0 1 0 1783991744 4657152 1051 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1137 1051 145 145 0 992 0
[pid=4669] vsize: 4548
Current children cumulated CPU time (s) 89.9
Current children cumulated vsize (Kb) 6672

[startup+100.014 s]
Raw data (loadavg): 0.86 0.71 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1105 0 0 0 9980 9 0 0 25 0 1 0 1783991744 4829184 1092 4294967295 134512640 135094434 3221224448 3221223112 134562037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1179 1092 145 145 0 1034 0
[pid=4669] vsize: 4716
Current children cumulated CPU time (s) 99.9
Current children cumulated vsize (Kb) 6840

[startup+110.015 s]
Raw data (loadavg): 0.88 0.72 0.83 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1111 0 0 0 10979 10 0 0 25 0 1 0 1783991744 4853760 1098 4294967295 134512640 135094434 3221224448 3221223100 134562168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1185 1098 145 145 0 1040 0
[pid=4669] vsize: 4740
Current children cumulated CPU time (s) 109.9
Current children cumulated vsize (Kb) 6864

[startup+120.017 s]
Raw data (loadavg): 0.90 0.73 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1169 0 0 0 11978 10 0 0 25 0 1 0 1783991744 5087232 1156 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1242 1156 145 145 0 1097 0
[pid=4669] vsize: 4968
Current children cumulated CPU time (s) 119.89
Current children cumulated vsize (Kb) 7092

[startup+130.017 s]
Raw data (loadavg): 0.92 0.74 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1209 0 0 0 12977 11 0 0 25 0 1 0 1783991744 5251072 1196 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1282 1196 145 145 0 1137 0
[pid=4669] vsize: 5128
Current children cumulated CPU time (s) 129.89
Current children cumulated vsize (Kb) 7252

[startup+140.018 s]
Raw data (loadavg): 0.93 0.74 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1227 0 0 0 13976 12 0 0 25 0 1 0 1783991744 5324800 1214 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1300 1214 145 145 0 1155 0
[pid=4669] vsize: 5200
Current children cumulated CPU time (s) 139.89
Current children cumulated vsize (Kb) 7324

[startup+150.02 s]
Raw data (loadavg): 0.94 0.75 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1248 0 0 0 14976 12 0 0 25 0 1 0 1783991744 5414912 1235 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1322 1235 145 145 0 1177 0
[pid=4669] vsize: 5288
Current children cumulated CPU time (s) 149.89
Current children cumulated vsize (Kb) 7412

[startup+160.021 s]
Raw data (loadavg): 0.95 0.76 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1261 0 0 0 15976 13 0 0 25 0 1 0 1783991744 5468160 1248 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1335 1248 145 145 0 1190 0
[pid=4669] vsize: 5340
Current children cumulated CPU time (s) 159.9
Current children cumulated vsize (Kb) 7464

[startup+170.022 s]
Raw data (loadavg): 0.95 0.77 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1274 0 0 0 16976 13 0 0 25 0 1 0 1783991744 5529600 1261 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1350 1261 145 145 0 1205 0
[pid=4669] vsize: 5400
Current children cumulated CPU time (s) 169.9
Current children cumulated vsize (Kb) 7524

[startup+180.023 s]
Raw data (loadavg): 0.96 0.77 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1279 0 0 0 17975 14 0 0 25 0 1 0 1783991744 5554176 1266 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1356 1266 145 145 0 1211 0
[pid=4669] vsize: 5424
Current children cumulated CPU time (s) 179.9
Current children cumulated vsize (Kb) 7548

[startup+190.024 s]
Raw data (loadavg): 0.97 0.78 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1342 0 0 0 18974 14 0 0 25 0 1 0 1783991744 5812224 1329 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1419 1329 145 145 0 1274 0
[pid=4669] vsize: 5676
Current children cumulated CPU time (s) 189.89
Current children cumulated vsize (Kb) 7800

[startup+200.026 s]
Raw data (loadavg): 0.97 0.79 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1382 0 0 0 19973 15 0 0 25 0 1 0 1783991744 5980160 1369 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1460 1369 145 145 0 1315 0
[pid=4669] vsize: 5840
Current children cumulated CPU time (s) 199.89
Current children cumulated vsize (Kb) 7964

[startup+210.026 s]
Raw data (loadavg): 0.98 0.79 0.84 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1397 0 0 0 20973 15 0 0 25 0 1 0 1783991744 6037504 1384 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1474 1384 145 145 0 1329 0
[pid=4669] vsize: 5896
Current children cumulated CPU time (s) 209.89
Current children cumulated vsize (Kb) 8020

[startup+220.028 s]
Raw data (loadavg): 0.98 0.80 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1410 0 0 0 21972 16 0 0 25 0 1 0 1783991744 6103040 1397 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1490 1397 145 145 0 1345 0
[pid=4669] vsize: 5960
Current children cumulated CPU time (s) 219.89
Current children cumulated vsize (Kb) 8084

[startup+230.029 s]
Raw data (loadavg): 0.98 0.81 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1419 0 0 0 22972 16 0 0 25 0 1 0 1783991744 6144000 1406 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1500 1406 145 145 0 1355 0
[pid=4669] vsize: 6000
Current children cumulated CPU time (s) 229.89
Current children cumulated vsize (Kb) 8124

[startup+240.03 s]
Raw data (loadavg): 0.98 0.81 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1428 0 0 0 23972 16 0 0 25 0 1 0 1783991744 6184960 1415 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1510 1415 145 145 0 1365 0
[pid=4669] vsize: 6040
Current children cumulated CPU time (s) 239.89
Current children cumulated vsize (Kb) 8164

[startup+250.031 s]
Raw data (loadavg): 0.99 0.82 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1438 0 0 0 24971 17 0 0 25 0 1 0 1783991744 6234112 1425 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1522 1425 145 145 0 1377 0
[pid=4669] vsize: 6088
Current children cumulated CPU time (s) 249.89
Current children cumulated vsize (Kb) 8212

[startup+260.032 s]
Raw data (loadavg): 0.99 0.82 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1443 0 0 0 25971 17 0 0 25 0 1 0 1783991744 6254592 1430 4294967295 134512640 135094434 3221224448 3221223120 134555837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1527 1430 145 145 0 1382 0
[pid=4669] vsize: 6108
Current children cumulated CPU time (s) 259.89
Current children cumulated vsize (Kb) 8232

[startup+270.033 s]
Raw data (loadavg): 0.99 0.83 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1462 0 0 0 26971 17 0 0 25 0 1 0 1783991744 6344704 1449 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1549 1449 145 145 0 1404 0
[pid=4669] vsize: 6196
Current children cumulated CPU time (s) 269.89
Current children cumulated vsize (Kb) 8320

[startup+280.034 s]
Raw data (loadavg): 0.99 0.83 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1484 0 0 0 27971 17 0 0 25 0 1 0 1783991744 6430720 1471 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1570 1471 145 145 0 1425 0
[pid=4669] vsize: 6280
Current children cumulated CPU time (s) 279.89
Current children cumulated vsize (Kb) 8404

[startup+290.035 s]
Raw data (loadavg): 0.99 0.84 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1520 0 0 0 28971 18 0 0 25 0 1 0 1783991744 6586368 1507 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 1608 1507 145 145 0 1463 0
[pid=4669] vsize: 6432
Current children cumulated CPU time (s) 289.9
Current children cumulated vsize (Kb) 8556

[startup+300.035 s]
Raw data (loadavg): 0.99 0.84 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1555 0 0 0 29970 18 0 0 25 0 1 0 1783991744 6729728 1542 4294967295 134512640 135094434 3221224448 3221223072 134557587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1643 1542 145 145 0 1498 0
[pid=4669] vsize: 6572
Current children cumulated CPU time (s) 299.89
Current children cumulated vsize (Kb) 8696

[startup+310.036 s]
Raw data (loadavg): 0.99 0.85 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1589 0 0 0 30970 18 0 0 25 0 1 0 1783991744 6877184 1576 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1679 1576 145 145 0 1534 0
[pid=4669] vsize: 6716
Current children cumulated CPU time (s) 309.89
Current children cumulated vsize (Kb) 8840

[startup+320.037 s]
Raw data (loadavg): 0.99 0.85 0.85 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1593 0 0 0 31971 18 0 0 25 0 1 0 1783991744 6893568 1580 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1683 1580 145 145 0 1538 0
[pid=4669] vsize: 6732
Current children cumulated CPU time (s) 319.9
Current children cumulated vsize (Kb) 8856

[startup+330.038 s]
Raw data (loadavg): 0.99 0.86 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1602 0 0 0 32971 18 0 0 25 0 1 0 1783991744 6934528 1589 4294967295 134512640 135094434 3221224448 3221223136 134554676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1693 1589 145 145 0 1548 0
[pid=4669] vsize: 6772
Current children cumulated CPU time (s) 329.9
Current children cumulated vsize (Kb) 8896

[startup+340.038 s]
Raw data (loadavg): 0.99 0.86 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1610 0 0 0 33971 18 0 0 25 0 1 0 1783991744 6967296 1597 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1701 1597 145 145 0 1556 0
[pid=4669] vsize: 6804
Current children cumulated CPU time (s) 339.9
Current children cumulated vsize (Kb) 8928

[startup+350.039 s]
Raw data (loadavg): 0.99 0.86 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1620 0 0 0 34971 18 0 0 25 0 1 0 1783991744 7008256 1607 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1711 1607 145 145 0 1566 0
[pid=4669] vsize: 6844
Current children cumulated CPU time (s) 349.9
Current children cumulated vsize (Kb) 8968

[startup+360.04 s]
Raw data (loadavg): 0.99 0.87 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1632 0 0 0 35971 18 0 0 25 0 1 0 1783991744 7065600 1619 4294967295 134512640 135094434 3221224448 3221223020 134562036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1725 1619 145 145 0 1580 0
[pid=4669] vsize: 6900
Current children cumulated CPU time (s) 359.9
Current children cumulated vsize (Kb) 9024

[startup+370.041 s]
Raw data (loadavg): 0.99 0.87 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1659 0 0 0 36971 18 0 0 25 0 1 0 1783991744 7184384 1646 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1754 1646 145 145 0 1609 0
[pid=4669] vsize: 7016
Current children cumulated CPU time (s) 369.9
Current children cumulated vsize (Kb) 9140

[startup+380.041 s]
Raw data (loadavg): 0.99 0.88 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1663 0 0 0 37971 18 0 0 25 0 1 0 1783991744 7200768 1650 4294967295 134512640 135094434 3221224448 3221223104 134558298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1758 1650 145 145 0 1613 0
[pid=4669] vsize: 7032
Current children cumulated CPU time (s) 379.9
Current children cumulated vsize (Kb) 9156

[startup+390.042 s]
Raw data (loadavg): 0.99 0.88 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1670 0 0 0 38972 18 0 0 25 0 1 0 1783991744 7233536 1657 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1766 1657 145 145 0 1621 0
[pid=4669] vsize: 7064
Current children cumulated CPU time (s) 389.91
Current children cumulated vsize (Kb) 9188

[startup+400.043 s]
Raw data (loadavg): 0.99 0.88 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1681 0 0 0 39971 18 0 0 25 0 1 0 1783991744 7278592 1668 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1777 1668 145 145 0 1632 0
[pid=4669] vsize: 7108
Current children cumulated CPU time (s) 399.9
Current children cumulated vsize (Kb) 9232

[startup+410.044 s]
Raw data (loadavg): 0.99 0.89 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1698 0 0 0 40971 18 0 0 25 0 1 0 1783991744 7352320 1685 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1795 1685 145 145 0 1650 0
[pid=4669] vsize: 7180
Current children cumulated CPU time (s) 409.9
Current children cumulated vsize (Kb) 9304

[startup+420.045 s]
Raw data (loadavg): 0.99 0.89 0.86 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1702 0 0 0 41972 19 0 0 25 0 1 0 1783991744 7368704 1689 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1799 1689 145 145 0 1654 0
[pid=4669] vsize: 7196
Current children cumulated CPU time (s) 419.92
Current children cumulated vsize (Kb) 9320

[startup+430.045 s]
Raw data (loadavg): 0.99 0.89 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1714 0 0 0 42972 19 0 0 25 0 1 0 1783991744 7417856 1701 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1811 1701 145 145 0 1666 0
[pid=4669] vsize: 7244
Current children cumulated CPU time (s) 429.92
Current children cumulated vsize (Kb) 9368

[startup+440.045 s]
Raw data (loadavg): 0.99 0.90 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1715 0 0 0 43972 19 0 0 25 0 1 0 1783991744 7417856 1702 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1811 1702 145 145 0 1666 0
[pid=4669] vsize: 7244
Current children cumulated CPU time (s) 439.92
Current children cumulated vsize (Kb) 9368

[startup+450.046 s]
Raw data (loadavg): 0.99 0.90 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1722 0 0 0 44972 19 0 0 25 0 1 0 1783991744 7450624 1709 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1819 1709 145 145 0 1674 0
[pid=4669] vsize: 7276
Current children cumulated CPU time (s) 449.92
Current children cumulated vsize (Kb) 9400

[startup+460.047 s]
Raw data (loadavg): 0.99 0.90 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1780 0 0 0 45970 20 0 0 25 0 1 0 1783991744 7688192 1767 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1877 1767 145 145 0 1732 0
[pid=4669] vsize: 7508
Current children cumulated CPU time (s) 459.91
Current children cumulated vsize (Kb) 9632

[startup+470.048 s]
Raw data (loadavg): 0.99 0.90 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1794 0 0 0 46970 20 0 0 25 0 1 0 1783991744 7749632 1781 4294967295 134512640 135094434 3221224448 3221223008 134562041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1892 1781 145 145 0 1747 0
[pid=4669] vsize: 7568
Current children cumulated CPU time (s) 469.91
Current children cumulated vsize (Kb) 9692

[startup+480.049 s]
Raw data (loadavg): 0.99 0.91 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1814 0 0 0 47970 20 0 0 25 0 1 0 1783991744 7835648 1801 4294967295 134512640 135094434 3221224448 3221223088 134539493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1913 1801 145 145 0 1768 0
[pid=4669] vsize: 7652
Current children cumulated CPU time (s) 479.91
Current children cumulated vsize (Kb) 9776

[startup+490.05 s]
Raw data (loadavg): 0.99 0.91 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1831 0 0 0 48970 20 0 0 25 0 1 0 1783991744 7917568 1818 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1933 1818 145 145 0 1788 0
[pid=4669] vsize: 7732
Current children cumulated CPU time (s) 489.91
Current children cumulated vsize (Kb) 9856

[startup+500.051 s]
Raw data (loadavg): 0.99 0.91 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1832 0 0 0 49971 20 0 0 25 0 1 0 1783991744 7917568 1819 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1933 1819 145 145 0 1788 0
[pid=4669] vsize: 7732
Current children cumulated CPU time (s) 499.92
Current children cumulated vsize (Kb) 9856

[startup+510.051 s]
Raw data (loadavg): 0.99 0.91 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1842 0 0 0 50971 21 0 0 25 0 1 0 1783991744 7954432 1829 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1942 1829 145 145 0 1797 0
[pid=4669] vsize: 7768
Current children cumulated CPU time (s) 509.93
Current children cumulated vsize (Kb) 9892

[startup+520.052 s]
Raw data (loadavg): 0.99 0.92 0.87 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1847 0 0 0 51970 21 0 0 25 0 1 0 1783991744 7970816 1834 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1946 1834 145 145 0 1801 0
[pid=4669] vsize: 7784
Current children cumulated CPU time (s) 519.92
Current children cumulated vsize (Kb) 9908

[startup+530.053 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1867 0 0 0 52970 21 0 0 25 0 1 0 1783991744 8056832 1854 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1967 1854 145 145 0 1822 0
[pid=4669] vsize: 7868
Current children cumulated CPU time (s) 529.92
Current children cumulated vsize (Kb) 9992

[startup+540.053 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1872 0 0 0 53970 21 0 0 25 0 1 0 1783991744 8081408 1859 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1973 1859 145 145 0 1828 0
[pid=4669] vsize: 7892
Current children cumulated CPU time (s) 539.92
Current children cumulated vsize (Kb) 10016

[startup+550.053 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1875 0 0 0 54971 21 0 0 25 0 1 0 1783991744 8097792 1862 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1977 1862 145 145 0 1832 0
[pid=4669] vsize: 7908
Current children cumulated CPU time (s) 549.93
Current children cumulated vsize (Kb) 10032

[startup+560.054 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1885 0 0 0 55971 21 0 0 25 0 1 0 1783991744 8146944 1872 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1989 1872 145 145 0 1844 0
[pid=4669] vsize: 7956
Current children cumulated CPU time (s) 559.93
Current children cumulated vsize (Kb) 10080

[startup+570.056 s]
Raw data (loadavg): 0.99 0.93 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1888 0 0 0 56971 21 0 0 25 0 1 0 1783991744 8163328 1875 4294967295 134512640 135094434 3221224448 3221223088 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1993 1875 145 145 0 1848 0
[pid=4669] vsize: 7972
Current children cumulated CPU time (s) 569.93
Current children cumulated vsize (Kb) 10096

[startup+580.057 s]
Raw data (loadavg): 0.99 0.93 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1891 0 0 0 57971 21 0 0 25 0 1 0 1783991744 8179712 1878 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 1997 1878 145 145 0 1852 0
[pid=4669] vsize: 7988
Current children cumulated CPU time (s) 579.93
Current children cumulated vsize (Kb) 10112

[startup+590.058 s]
Raw data (loadavg): 0.99 0.93 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1897 0 0 0 58971 21 0 0 25 0 1 0 1783991744 8204288 1884 4294967295 134512640 135094434 3221224448 3221223088 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2003 1884 145 145 0 1858 0
[pid=4669] vsize: 8012
Current children cumulated CPU time (s) 589.93
Current children cumulated vsize (Kb) 10136

[startup+600.059 s]
Raw data (loadavg): 0.99 0.93 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1911 0 0 0 59971 21 0 0 25 0 1 0 1783991744 8265728 1898 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2018 1898 145 145 0 1873 0
[pid=4669] vsize: 8072
Current children cumulated CPU time (s) 599.93
Current children cumulated vsize (Kb) 10196

[startup+610.059 s]
Raw data (loadavg): 0.99 0.93 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1919 0 0 0 60972 21 0 0 25 0 1 0 1783991744 8298496 1906 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2026 1906 145 145 0 1881 0
[pid=4669] vsize: 8104
Current children cumulated CPU time (s) 609.94
Current children cumulated vsize (Kb) 10228

[startup+620.06 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1931 0 0 0 61971 21 0 0 25 0 1 0 1783991744 8347648 1918 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2038 1918 145 145 0 1893 0
[pid=4669] vsize: 8152
Current children cumulated CPU time (s) 619.93
Current children cumulated vsize (Kb) 10276

[startup+630.061 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1931 0 0 0 62972 21 0 0 25 0 1 0 1783991744 8347648 1918 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2038 1918 145 145 0 1893 0
[pid=4669] vsize: 8152
Current children cumulated CPU time (s) 629.94
Current children cumulated vsize (Kb) 10276

[startup+640.061 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1934 0 0 0 63972 21 0 0 25 0 1 0 1783991744 8364032 1921 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2042 1921 145 145 0 1897 0
[pid=4669] vsize: 8168
Current children cumulated CPU time (s) 639.94
Current children cumulated vsize (Kb) 10292

[startup+650.062 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1940 0 0 0 64972 21 0 0 25 0 1 0 1783991744 8396800 1927 4294967295 134512640 135094434 3221224448 3221222912 134781514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2050 1927 145 145 0 1905 0
[pid=4669] vsize: 8200
Current children cumulated CPU time (s) 649.94
Current children cumulated vsize (Kb) 10324

[startup+660.063 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1948 0 0 0 65972 21 0 0 25 0 1 0 1783991744 8433664 1935 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2059 1935 145 145 0 1914 0
[pid=4669] vsize: 8236
Current children cumulated CPU time (s) 659.94
Current children cumulated vsize (Kb) 10360

[startup+670.065 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1953 0 0 0 66973 21 0 0 25 0 1 0 1783991744 8458240 1940 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2065 1940 145 145 0 1920 0
[pid=4669] vsize: 8260
Current children cumulated CPU time (s) 669.95
Current children cumulated vsize (Kb) 10384

[startup+680.066 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1959 0 0 0 67973 21 0 0 25 0 1 0 1783991744 8491008 1946 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2073 1946 145 145 0 1928 0
[pid=4669] vsize: 8292
Current children cumulated CPU time (s) 679.95
Current children cumulated vsize (Kb) 10416

[startup+690.066 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1965 0 0 0 68973 21 0 0 25 0 1 0 1783991744 8523776 1952 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2081 1952 145 145 0 1936 0
[pid=4669] vsize: 8324
Current children cumulated CPU time (s) 689.95
Current children cumulated vsize (Kb) 10448

[startup+700.067 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1968 0 0 0 69973 21 0 0 25 0 1 0 1783991744 8531968 1955 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2083 1955 145 145 0 1938 0
[pid=4669] vsize: 8332
Current children cumulated CPU time (s) 699.95
Current children cumulated vsize (Kb) 10456

[startup+710.068 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 1971 0 0 0 70973 21 0 0 25 0 1 0 1783991744 8548352 1958 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2087 1958 145 145 0 1942 0
[pid=4669] vsize: 8348
Current children cumulated CPU time (s) 709.95
Current children cumulated vsize (Kb) 10472

[startup+720.069 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2018 0 0 0 71972 22 0 0 25 0 1 0 1783991744 8740864 2005 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 2134 2005 145 145 0 1989 0
[pid=4669] vsize: 8536
Current children cumulated CPU time (s) 719.95
Current children cumulated vsize (Kb) 10660

[startup+730.07 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2041 0 0 0 72972 22 0 0 25 0 1 0 1783991744 8835072 2028 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2157 2028 145 145 0 2012 0
[pid=4669] vsize: 8628
Current children cumulated CPU time (s) 729.95
Current children cumulated vsize (Kb) 10752

[startup+740.071 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2047 0 0 0 73972 22 0 0 25 0 1 0 1783991744 8867840 2034 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2165 2034 145 145 0 2020 0
[pid=4669] vsize: 8660
Current children cumulated CPU time (s) 739.95
Current children cumulated vsize (Kb) 10784

[startup+750.072 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2063 0 0 0 74972 22 0 0 25 0 1 0 1783991744 8929280 2050 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2180 2050 145 145 0 2035 0
[pid=4669] vsize: 8720
Current children cumulated CPU time (s) 749.95
Current children cumulated vsize (Kb) 10844

[startup+760.073 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2072 0 0 0 75971 22 0 0 25 0 1 0 1783991744 8970240 2059 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2190 2059 145 145 0 2045 0
[pid=4669] vsize: 8760
Current children cumulated CPU time (s) 759.94
Current children cumulated vsize (Kb) 10884

[startup+770.074 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2109 0 0 0 76971 22 0 0 25 0 1 0 1783991744 9125888 2096 4294967295 134512640 135094434 3221224448 3221223088 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2228 2096 145 145 0 2083 0
[pid=4669] vsize: 8912
Current children cumulated CPU time (s) 769.94
Current children cumulated vsize (Kb) 11036

[startup+780.075 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2112 0 0 0 77971 22 0 0 25 0 1 0 1783991744 9142272 2099 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2232 2099 145 145 0 2087 0
[pid=4669] vsize: 8928
Current children cumulated CPU time (s) 779.94
Current children cumulated vsize (Kb) 11052

[startup+790.076 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2112 0 0 0 78972 22 0 0 25 0 1 0 1783991744 9142272 2099 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2232 2099 145 145 0 2087 0
[pid=4669] vsize: 8928
Current children cumulated CPU time (s) 789.95
Current children cumulated vsize (Kb) 11052

[startup+800.077 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2115 0 0 0 79972 22 0 0 25 0 1 0 1783991744 9158656 2102 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2236 2102 145 145 0 2091 0
[pid=4669] vsize: 8944
Current children cumulated CPU time (s) 799.95
Current children cumulated vsize (Kb) 11068

[startup+810.077 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2119 0 0 0 80972 22 0 0 25 0 1 0 1783991744 9175040 2106 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2240 2106 145 145 0 2095 0
[pid=4669] vsize: 8960
Current children cumulated CPU time (s) 809.95
Current children cumulated vsize (Kb) 11084

[startup+820.078 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2124 0 0 0 81972 23 0 0 25 0 1 0 1783991744 9207808 2111 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2248 2111 145 145 0 2103 0
[pid=4669] vsize: 8992
Current children cumulated CPU time (s) 819.96
Current children cumulated vsize (Kb) 11116

[startup+830.079 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2124 0 0 0 82972 23 0 0 25 0 1 0 1783991744 9207808 2111 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2248 2111 145 145 0 2103 0
[pid=4669] vsize: 8992
Current children cumulated CPU time (s) 829.96
Current children cumulated vsize (Kb) 11116

[startup+840.08 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2124 0 0 0 83973 23 0 0 25 0 1 0 1783991744 9207808 2111 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2248 2111 145 145 0 2103 0
[pid=4669] vsize: 8992
Current children cumulated CPU time (s) 839.97
Current children cumulated vsize (Kb) 11116

[startup+850.081 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2129 0 0 0 84972 23 0 0 25 0 1 0 1783991744 9232384 2116 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2254 2116 145 145 0 2109 0
[pid=4669] vsize: 9016
Current children cumulated CPU time (s) 849.96
Current children cumulated vsize (Kb) 11140

[startup+860.08 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2144 0 0 0 85972 23 0 0 25 0 1 0 1783991744 9289728 2131 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2268 2131 145 145 0 2123 0
[pid=4669] vsize: 9072
Current children cumulated CPU time (s) 859.96
Current children cumulated vsize (Kb) 11196

[startup+870.082 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2146 0 0 0 86973 23 0 0 25 0 1 0 1783991744 9297920 2133 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2270 2133 145 145 0 2125 0
[pid=4669] vsize: 9080
Current children cumulated CPU time (s) 869.97
Current children cumulated vsize (Kb) 11204

[startup+880.083 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2155 0 0 0 87973 23 0 0 25 0 1 0 1783991744 9342976 2142 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2281 2142 145 145 0 2136 0
[pid=4669] vsize: 9124
Current children cumulated CPU time (s) 879.97
Current children cumulated vsize (Kb) 11248

[startup+890.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2155 0 0 0 88973 23 0 0 25 0 1 0 1783991744 9342976 2142 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2281 2142 145 145 0 2136 0
[pid=4669] vsize: 9124
Current children cumulated CPU time (s) 889.97
Current children cumulated vsize (Kb) 11248

[startup+900.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2159 0 0 0 89973 23 0 0 25 0 1 0 1783991744 9359360 2146 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2285 2146 145 145 0 2140 0
[pid=4669] vsize: 9140
Current children cumulated CPU time (s) 899.97
Current children cumulated vsize (Kb) 11264

[startup+910.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2168 0 0 0 90973 23 0 0 25 0 1 0 1783991744 9400320 2155 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2295 2155 145 145 0 2150 0
[pid=4669] vsize: 9180
Current children cumulated CPU time (s) 909.97
Current children cumulated vsize (Kb) 11304

[startup+920.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2192 0 0 0 91973 24 0 0 25 0 1 0 1783991744 9498624 2179 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2319 2179 145 145 0 2174 0
[pid=4669] vsize: 9276
Current children cumulated CPU time (s) 919.98
Current children cumulated vsize (Kb) 11400

[startup+930.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2196 0 0 0 92973 24 0 0 25 0 1 0 1783991744 9515008 2183 4294967295 134512640 135094434 3221224448 3221223104 134557987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2323 2183 145 145 0 2178 0
[pid=4669] vsize: 9292
Current children cumulated CPU time (s) 929.98
Current children cumulated vsize (Kb) 11416

[startup+940.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2198 0 0 0 93973 24 0 0 25 0 1 0 1783991744 9515008 2185 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2323 2185 145 145 0 2178 0
[pid=4669] vsize: 9292
Current children cumulated CPU time (s) 939.98
Current children cumulated vsize (Kb) 11416

[startup+950.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2201 0 0 0 94973 24 0 0 25 0 1 0 1783991744 9531392 2188 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2327 2188 145 145 0 2182 0
[pid=4669] vsize: 9308
Current children cumulated CPU time (s) 949.98
Current children cumulated vsize (Kb) 11432

[startup+960.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2206 0 0 0 95974 24 0 0 25 0 1 0 1783991744 9555968 2193 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2333 2193 145 145 0 2188 0
[pid=4669] vsize: 9332
Current children cumulated CPU time (s) 959.99
Current children cumulated vsize (Kb) 11456

[startup+970.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2210 0 0 0 96974 24 0 0 25 0 1 0 1783991744 9572352 2197 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2337 2197 145 145 0 2192 0
[pid=4669] vsize: 9348
Current children cumulated CPU time (s) 969.99
Current children cumulated vsize (Kb) 11472

[startup+980.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2211 0 0 0 97974 24 0 0 25 0 1 0 1783991744 9576448 2198 4294967295 134512640 135094434 3221224448 3221223040 134557178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2338 2198 145 145 0 2193 0
[pid=4669] vsize: 9352
Current children cumulated CPU time (s) 979.99
Current children cumulated vsize (Kb) 11476

[startup+990.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2229 0 0 0 98974 24 0 0 25 0 1 0 1783991744 9654272 2216 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2357 2216 145 145 0 2212 0
[pid=4669] vsize: 9428
Current children cumulated CPU time (s) 989.99
Current children cumulated vsize (Kb) 11552

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2229 0 0 0 99974 24 0 0 25 0 1 0 1783991744 9654272 2216 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2357 2216 145 145 0 2212 0
[pid=4669] vsize: 9428
Current children cumulated CPU time (s) 999.99
Current children cumulated vsize (Kb) 11552

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2232 0 0 0 100974 24 0 0 25 0 1 0 1783991744 9670656 2219 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2361 2219 145 145 0 2216 0
[pid=4669] vsize: 9444
Current children cumulated CPU time (s) 1009.99
Current children cumulated vsize (Kb) 11568

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2259 0 0 0 101974 24 0 0 25 0 1 0 1783991744 9781248 2246 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2388 2246 145 145 0 2243 0
[pid=4669] vsize: 9552
Current children cumulated CPU time (s) 1019.99
Current children cumulated vsize (Kb) 11676

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2276 0 0 0 102974 24 0 0 25 0 1 0 1783991744 9859072 2263 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2407 2263 145 145 0 2262 0
[pid=4669] vsize: 9628
Current children cumulated CPU time (s) 1029.99
Current children cumulated vsize (Kb) 11752

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2276 0 0 0 103974 24 0 0 25 0 1 0 1783991744 9859072 2263 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2407 2263 145 145 0 2262 0
[pid=4669] vsize: 9628
Current children cumulated CPU time (s) 1039.99
Current children cumulated vsize (Kb) 11752

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2280 0 0 0 104975 24 0 0 25 0 1 0 1783991744 9875456 2267 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2411 2267 145 145 0 2266 0
[pid=4669] vsize: 9644
Current children cumulated CPU time (s) 1050
Current children cumulated vsize (Kb) 11768

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2280 0 0 0 105975 24 0 0 25 0 1 0 1783991744 9875456 2267 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2411 2267 145 145 0 2266 0
[pid=4669] vsize: 9644
Current children cumulated CPU time (s) 1060
Current children cumulated vsize (Kb) 11768

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2281 0 0 0 106975 24 0 0 25 0 1 0 1783991744 9875456 2268 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2411 2268 145 145 0 2266 0
[pid=4669] vsize: 9644
Current children cumulated CPU time (s) 1070
Current children cumulated vsize (Kb) 11768

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2284 0 0 0 107975 24 0 0 25 0 1 0 1783991744 9891840 2271 4294967295 134512640 135094434 3221224448 3221223040 134551469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2415 2271 145 145 0 2270 0
[pid=4669] vsize: 9660
Current children cumulated CPU time (s) 1080
Current children cumulated vsize (Kb) 11784

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2284 0 0 0 108975 24 0 0 25 0 1 0 1783991744 9891840 2271 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2415 2271 145 145 0 2270 0
[pid=4669] vsize: 9660
Current children cumulated CPU time (s) 1090
Current children cumulated vsize (Kb) 11784

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2284 0 0 0 109976 24 0 0 25 0 1 0 1783991744 9891840 2271 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2415 2271 145 145 0 2270 0
[pid=4669] vsize: 9660
Current children cumulated CPU time (s) 1100.01
Current children cumulated vsize (Kb) 11784

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2291 0 0 0 110975 24 0 0 25 0 1 0 1783991744 9924608 2278 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 2423 2278 145 145 0 2278 0
[pid=4669] vsize: 9692
Current children cumulated CPU time (s) 1110
Current children cumulated vsize (Kb) 11816

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2297 0 0 0 111974 25 0 0 25 0 1 0 1783991744 9957376 2284 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2431 2284 145 145 0 2286 0
[pid=4669] vsize: 9724
Current children cumulated CPU time (s) 1120
Current children cumulated vsize (Kb) 11848

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2303 0 0 0 112974 25 0 0 25 0 1 0 1783991744 9981952 2290 4294967295 134512640 135094434 3221224448 3221223104 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2437 2290 145 145 0 2292 0
[pid=4669] vsize: 9748
Current children cumulated CPU time (s) 1130
Current children cumulated vsize (Kb) 11872

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2323 0 0 0 113972 26 0 0 25 0 1 0 1783991744 10059776 2310 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 2456 2310 145 145 0 2311 0
[pid=4669] vsize: 9824
Current children cumulated CPU time (s) 1139.99
Current children cumulated vsize (Kb) 11948

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2336 0 0 0 114971 27 0 0 25 0 1 0 1783991744 10113024 2323 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4669/statm): 2469 2323 145 145 0 2324 0
[pid=4669] vsize: 9876
Current children cumulated CPU time (s) 1149.99
Current children cumulated vsize (Kb) 12000

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2342 0 0 0 115970 28 0 0 25 0 1 0 1783991744 10133504 2329 4294967295 134512640 135094434 3221224448 3221222912 134781090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2474 2329 145 145 0 2329 0
[pid=4669] vsize: 9896
Current children cumulated CPU time (s) 1159.99
Current children cumulated vsize (Kb) 12020

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2350 0 0 0 116970 28 0 0 25 0 1 0 1783991744 10166272 2337 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2482 2337 145 145 0 2337 0
[pid=4669] vsize: 9928
Current children cumulated CPU time (s) 1169.99
Current children cumulated vsize (Kb) 12052

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2350 0 0 0 117970 28 0 0 25 0 1 0 1783991744 10166272 2337 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2482 2337 145 145 0 2337 0
[pid=4669] vsize: 9928
Current children cumulated CPU time (s) 1179.99
Current children cumulated vsize (Kb) 12052

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2354 0 0 0 118970 28 0 0 25 0 1 0 1783991744 10182656 2341 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2486 2341 145 145 0 2341 0
[pid=4669] vsize: 9944
Current children cumulated CPU time (s) 1189.99
Current children cumulated vsize (Kb) 12068

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2362 0 0 0 119971 28 0 0 25 0 1 0 1783991744 10215424 2349 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2494 2349 145 145 0 2349 0
[pid=4669] vsize: 9976
Current children cumulated CPU time (s) 1200
Current children cumulated vsize (Kb) 12100



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4669
Raw data (/proc/4665/stat): 4665 (minisat+_script) S 4664 4665 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1783991739 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4665/statm): 531 226 485 147 0 384 0
[pid=4665] vsize: 2124
Raw data (/proc/4669/stat): 4669 (minisat+_64-bit) R 4665 4665 30740 0 -1 0 2362 0 0 0 119971 28 0 0 25 0 1 0 1783991744 10215424 2349 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4669/statm): 2494 2349 145 145 0 2349 0
[pid=4669] vsize: 9976
Current children cumulated CPU time (s) 1200
Current children cumulated vsize (Kb) 12100

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

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200
CPU user time (s): 1199.71
CPU system time (s): 0.287956
CPU usage (%): 99.9902
Max. virtual memory (cumulated for all children) (Kb): 12100

Verifier Data

ERROR: no interpretation found !