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

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb45-21-opb/normalized-frb45-21-3.opb
MD5SUMb3a3f977e810fc2043ea057a8d94a7d8
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -37
Optimality of the best value was proved NO
Number of terms in the objective function 945
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 945
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 945
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.04
Number of variables945
Total number of constraints58245
Number of constraints which are clauses58245
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 constraint2

Trace number 2300

Launcher Data

LAUNCH ON wulflinc4 THE 2005-09-18 18:47:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2704 boxname=wulflinc4 idbench=360 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b3a3f977e810fc2043ea057a8d94a7d8  /oldhome/oroussel/tmp/wulflinc4/normalized-frb45-21-3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-frb45-21-3.opb
IDLAUNCH: 2704
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        919144 kB
Buffers:         34904 kB
Cached:          56480 kB
SwapCached:        960 kB
Active:          66060 kB
Inactive:        27948 kB
HighTotal:      131008 kB
HighFree:        72156 kB
LowTotal:       903652 kB
LowFree:        846988 kB
SwapTotal:     2097136 kB
SwapFree:      2095628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            15728 kB
Committed_AS:    72324 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:07:31 (client local time) WITH STATUS 10 IN 1208.42 SECONDS
stats: 2704 7 1208.42 10

Solver Data

c Parsing PB file...
c Converting 58245 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 |   58245   116490 |   19415       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -29
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  103674   223173 |   34558       0        0     nan |  0.000 % |
c |       100 |  103217   222224 |   38013      74      640     8.6 |  0.795 % |
c |       250 |  102277   220190 |   41815     178     1328     7.5 |  2.556 % |
c |       475 |  101299   218072 |   45996     363     3330     9.2 |  4.391 % |
c |       812 |   99047   213116 |   50596     601     6292    10.5 |  8.826 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1154 |   97981   210998 |   32660     842     9717    11.5 |  8.826 % |
c |      1254 |   97456   209833 |   35926     908    10864    12.0 | 12.242 % |
c |      1404 |   96930   208673 |   39518    1038    12408    12.0 | 13.257 % |
c |      1630 |   96171   206966 |   43470    1223    14347    11.7 | 14.977 % |
c |      1967 |   94090   202274 |   47817    1458    16260    11.2 | 18.956 % |
c |      2473 |   92212   198058 |   52599    1787    19115    10.7 | 22.689 % |
c |      3232 |   88553   189636 |   57859    2356    25138    10.7 | 30.105 % |
c |      4372 |   84300   179875 |   63645    3005    31878    10.6 | 38.823 % |
c |      6081 |   80620   171309 |   70009    4307    46466    10.8 | 46.451 % |
c |      8643 |   75017   158019 |   77010    6013    68321    11.4 | 58.474 % |
c ==============================================================================
c Found solution: -34
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9837 |   73511   154433 |   24503    6917    84271    12.2 | 58.474 % |
c |      9937 |   73160   153606 |   26953    6916    84599    12.2 | 62.459 % |
c |     10087 |   73060   153368 |   29648    6999    85824    12.3 | 62.676 % |
c |     10312 |   72828   152824 |   32613    7170    89136    12.4 | 63.163 % |
c |     10649 |   72659   152439 |   35874    7471    94516    12.7 | 63.509 % |
c |     11155 |   72503   152068 |   39462    7865   103845    13.2 | 63.970 % |
c |     11914 |   71669   150067 |   43408    8396   115466    13.8 | 65.675 % |
c |     13055 |   71037   148549 |   47749    9401   141983    15.1 | 67.046 % |
c |     14763 |   70222   146623 |   52524   10862   187323    17.2 | 68.772 % |
c ==============================================================================
c Found solution: -35
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15084 |   70261   146790 |   23420   11142   194649    17.5 | 68.772 % |
c |     15184 |   70145   146515 |   25762   11226   196318    17.5 | 69.049 % |
c |     15334 |   70122   146458 |   28338   11375   199287    17.5 | 69.100 % |
c |     15559 |   70122   146458 |   31172   11600   219368    18.9 | 69.100 % |
c |     15896 |   70114   146440 |   34289   11935   226983    19.0 | 69.116 % |
c |     16402 |   69855   145806 |   37718   12327   241011    19.6 | 69.697 % |
c |     17161 |   69457   144856 |   41489   12860   269839    21.0 | 70.553 % |
c |     18300 |   68230   141868 |   45638   13498   300688    22.3 | 73.307 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19394 |   67923   141108 |   22641   14427   343281    23.8 | 73.307 % |
c |     19495 |   67908   141073 |   24905   14526   347004    23.9 | 74.024 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19613 |   67925   141145 |   22641   14641   351375    24.0 | 74.024 % |
c |     19713 |   67839   140937 |   24905   14731   356033    24.2 | 74.212 % |
c |     19863 |   67762   140750 |   27395   14851   358518    24.1 | 74.384 % |
c |     20088 |   67631   140425 |   30135   14979   363163    24.2 | 74.687 % |
c |     20425 |   67626   140412 |   33148   15243   374131    24.5 | 74.700 % |
c |     20932 |   67626   140412 |   36463   15750   434642    27.6 | 74.700 % |
c |     21692 |   67432   139937 |   40109   16429   458771    27.9 | 75.130 % |
c |     22831 |   67112   139167 |   44120   17411   506808    29.1 | 75.822 % |
c |     24539 |   67069   139072 |   48532   19055   591866    31.1 | 75.899 % |
c |     27101 |   66891   138638 |   53386   21563   774079    35.9 | 76.294 % |
c |     30945 |   66792   138391 |   58724   25311  1005599    39.7 | 76.527 % |
c ==============================================================================
c Found solution: -38
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35844 |   66669   138025 |   22223   30022  1470073    49.0 | 76.527 % |
c |     35945 |   66544   137727 |   24445   30030  1471559    49.0 | 77.089 % |
c |     36097 |   66544   137727 |   26889   30182  1483627    49.2 | 77.089 % |
c |     36322 |   66328   137202 |   29578   30294  1489137    49.2 | 77.568 % |
c |     36659 |   66286   137102 |   32536   30598  1502725    49.1 | 77.657 % |
c |     37165 |   66286   137102 |   35790   31104  1531065    49.2 | 77.657 % |
c |     37924 |   66236   136980 |   39369   31838  1579318    49.6 | 77.772 % |
c |     39063 |   66198   136896 |   43306   32931  1663184    50.5 | 77.845 % |
c |     40771 |   66094   136643 |   47636   34450  1773571    51.5 | 78.081 % |
c ==============================================================================
c Found solution: -39
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43229 |   66119   136738 |   22039   36846  2044619    55.5 | 78.081 % |
c |     43330 |   66082   136649 |   24242   36918  2046357    55.4 | 78.194 % |
c |     43480 |   66082   136649 |   26667   37068  2055234    55.4 | 78.194 % |
c |     43705 |   66061   136598 |   29333   37197  2068198    55.6 | 78.241 % |
c |     44042 |   66061   136598 |   32267   37534  2088672    55.6 | 78.241 % |
c |     44548 |   65988   136417 |   35494   37789  2109858    55.8 | 78.407 % |
c |     45307 |   65967   136364 |   39043   38528  2171262    56.4 | 78.457 % |
c |     46446 |   65967   136364 |   42947   39667  2284055    57.6 | 78.457 % |
c |     48155 |   65911   136232 |   47242   41326  2437988    59.0 | 78.578 % |
c |     50717 |   65911   136232 |   51966   43888  2766324    63.0 | 78.578 % |
c |     54561 |   65908   136225 |   57163   47731  3237086    67.8 | 78.584 % |
c ==============================================================================
c Found solution: -40
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56290 |   65823   135998 |   21941   48563  3297518    67.9 | 78.584 % |
c |     56390 |   65712   135748 |   24135   19988  1396674    69.9 | 78.983 % |
c |     56540 |   65712   135748 |   26548   20138  1404187    69.7 | 78.983 % |
c |     56765 |   65650   135596 |   29203   20338  1414088    69.5 | 79.126 % |
c |     57103 |   65650   135596 |   32123   20676  1442270    69.8 | 79.126 % |
c |     57610 |   65650   135596 |   35336   21183  1470803    69.4 | 79.126 % |
c |     58369 |   65650   135596 |   38869   21942  1512854    68.9 | 79.126 % |
c |     59509 |   65650   135596 |   42756   23082  1617718    70.1 | 79.126 % |
c |     61219 |   65650   135596 |   47032   24792  1814999    73.2 | 79.126 % |
c |     63781 |   65446   135086 |   51735   27327  2124510    77.7 | 79.590 % |
c |     67625 |   65344   134832 |   56909   31081  2420985    77.9 | 79.825 % |
c |     73391 |   65273   134642 |   62600   36808  2997370    81.4 | 80.003 % |
c ==============================================================================
c Found solution: -41
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78259 |   65233   134560 |   21744   41665  3434394    82.4 | 80.003 % |
c |     78359 |   65233   134560 |   23918   41765  3440374    82.4 | 80.114 % |
c |     78509 |   65194   134462 |   26310   41909  3446929    82.2 | 80.209 % |
c |     78735 |   65194   134462 |   28941   42135  3468085    82.3 | 80.209 % |
c |     79072 |   65194   134462 |   31835   42472  3491885    82.2 | 80.209 % |
c |     79578 |   65194   134462 |   35018   42978  3533426    82.2 | 80.209 % |
c |     80337 |   65194   134462 |   38520   43737  3606744    82.5 | 80.209 % |
c |     81476 |   65186   134442 |   42372   44835  3720600    83.0 | 80.228 % |
c |     83184 |   65186   134442 |   46610   46543  3854293    82.8 | 80.228 % |
c |     85747 |   65146   134350 |   51271   49094  4064252    82.8 | 80.307 % |
c |     89591 |   65137   134329 |   56398   52931  4435673    83.8 | 80.326 % |
c |     95358 |   65137   134329 |   62038   58698  5204836    88.7 | 80.326 % |
c |    104009 |   65137   134329 |   68241   67349  6225461    92.4 | 80.326 % |
c |    116985 |   65033   134076 |   75066   80299  7880223    98.1 | 80.561 % |
c |    136446 |   64945   133856 |   82572   99663 10505945   105.4 | 80.761 % |
c |    165638 |   64651   133139 |   90830   37553  3984323   106.1 | 81.418 % |
c |    209427 |   64398   132524 |   99913   81184  8603031   106.0 | 81.986 % |
c |    275112 |   64354   132420 |  109904   41677  3387232    81.3 | 82.081 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 C740 -C739 -C738 -C737 -C736 -C735 -C734 C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 C381 -C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265

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/16498/stat): 16498 (minisat+_script) R 16497 16498 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785288162 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16498/statm): 174 3 169 147 0 27 0
[pid=16498] 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=16499
New process pid=16500
New process pid=16501
execve syscall for /bin/sed executable
One traced child (pid=16500) 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=16501) exited with status: 0
One traced child (pid=16499) exited with status: 0
New process pid=16502
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-frb45-21-3.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 3710 0 0 0 968 15 0 0 25 0 1 0 1785288167 15609856 3697 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 3811 3697 145 145 0 3666 0
[pid=16502] vsize: 15244
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 17368

[startup+20.0051 s]
Raw data (loadavg): 0.94 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 3710 0 0 0 1967 15 0 0 25 0 1 0 1785288167 15609856 3697 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 3811 3697 145 145 0 3666 0
[pid=16502] vsize: 15244
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 17368

[startup+30.0069 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 3710 0 0 0 2966 16 0 0 25 0 1 0 1785288167 15609856 3697 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 3811 3697 145 145 0 3666 0
[pid=16502] vsize: 15244
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 17368

[startup+40.0078 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 3710 0 0 0 3965 16 0 0 25 0 1 0 1785288167 15609856 3697 4294967295 134512640 135094434 3221224448 3221223120 134553437 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 3811 3697 145 145 0 3666 0
[pid=16502] vsize: 15244
Current children cumulated CPU time (s) 39.81
Current children cumulated vsize (Kb) 17368

[startup+50.0086 s]
Raw data (loadavg): 0.96 0.96 0.94 3/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 3742 0 0 0 4964 17 0 0 25 0 1 0 1785288167 15704064 3729 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 3834 3729 145 145 0 3689 0
[pid=16502] vsize: 15336
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 17460

[startup+60.0095 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 4005 0 0 0 5959 19 0 0 25 0 1 0 1785288167 16617472 3952 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 4057 3952 145 145 0 3912 0
[pid=16502] vsize: 16228
Current children cumulated CPU time (s) 59.78
Current children cumulated vsize (Kb) 18352

[startup+70.0103 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 4474 0 0 0 6951 22 0 0 25 0 1 0 1785288167 18247680 4339 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 4455 4339 145 145 0 4310 0
[pid=16502] vsize: 17820
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 19944

[startup+80.0112 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 5006 0 0 0 7941 26 0 0 25 0 1 0 1785288167 20402176 4871 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 4981 4871 145 145 0 4836 0
[pid=16502] vsize: 19924
Current children cumulated CPU time (s) 79.67
Current children cumulated vsize (Kb) 22048

[startup+90.012 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 5530 0 0 0 8931 31 0 0 25 0 1 0 1785288167 22360064 5354 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 5459 5354 145 145 0 5314 0
[pid=16502] vsize: 21836
Current children cumulated CPU time (s) 89.62
Current children cumulated vsize (Kb) 23960

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 6003 0 0 0 9923 33 0 0 25 0 1 0 1785288167 24412160 5827 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 5960 5827 145 145 0 5815 0
[pid=16502] vsize: 23840
Current children cumulated CPU time (s) 99.56
Current children cumulated vsize (Kb) 25964

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 6460 0 0 0 10915 37 0 0 25 0 1 0 1785288167 26103808 6244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 6373 6244 145 145 0 6228 0
[pid=16502] vsize: 25492
Current children cumulated CPU time (s) 109.52
Current children cumulated vsize (Kb) 27616

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 6993 0 0 0 11906 41 0 0 25 0 1 0 1785288167 28270592 6777 4294967295 134512640 135094434 3221224448 3221223040 134557350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 6902 6777 145 145 0 6757 0
[pid=16502] vsize: 27608
Current children cumulated CPU time (s) 119.47
Current children cumulated vsize (Kb) 29732

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 7464 0 0 0 12897 45 0 0 25 0 1 0 1785288167 30183424 7248 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 7369 7248 145 145 0 7224 0
[pid=16502] vsize: 29476
Current children cumulated CPU time (s) 129.42
Current children cumulated vsize (Kb) 31600

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 7656 0 0 0 13895 46 0 0 25 0 1 0 1785288167 30801920 7400 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 7520 7400 145 145 0 7375 0
[pid=16502] vsize: 30080
Current children cumulated CPU time (s) 139.41
Current children cumulated vsize (Kb) 32204

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 7656 0 0 0 14895 46 0 0 25 0 1 0 1785288167 30801920 7400 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 7520 7400 145 145 0 7375 0
[pid=16502] vsize: 30080
Current children cumulated CPU time (s) 149.41
Current children cumulated vsize (Kb) 32204

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 7656 0 0 0 15895 46 0 0 25 0 1 0 1785288167 30801920 7400 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 7520 7400 145 145 0 7375 0
[pid=16502] vsize: 30080
Current children cumulated CPU time (s) 159.41
Current children cumulated vsize (Kb) 32204

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 7656 0 0 0 16895 46 0 0 25 0 1 0 1785288167 30801920 7400 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 7520 7400 145 145 0 7375 0
[pid=16502] vsize: 30080
Current children cumulated CPU time (s) 169.41
Current children cumulated vsize (Kb) 32204

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 7789 0 0 0 17893 47 0 0 25 0 1 0 1785288167 31178752 7492 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 7612 7492 145 145 0 7467 0
[pid=16502] vsize: 30448
Current children cumulated CPU time (s) 179.4
Current children cumulated vsize (Kb) 32572

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 8156 0 0 0 18887 50 0 0 25 0 1 0 1785288167 32681984 7859 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 7979 7859 145 145 0 7834 0
[pid=16502] vsize: 31916
Current children cumulated CPU time (s) 189.37
Current children cumulated vsize (Kb) 34040

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 8508 0 0 0 19880 53 0 0 25 0 1 0 1785288167 34123776 8211 4294967295 134512640 135094434 3221224448 3221223040 134557244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 8331 8211 145 145 0 8186 0
[pid=16502] vsize: 33324
Current children cumulated CPU time (s) 199.33
Current children cumulated vsize (Kb) 35448

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 8881 0 0 0 20873 55 0 0 25 0 1 0 1785288167 35639296 8584 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 8701 8584 145 145 0 8556 0
[pid=16502] vsize: 34804
Current children cumulated CPU time (s) 209.28
Current children cumulated vsize (Kb) 36928

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 9394 0 0 0 21863 59 0 0 25 0 1 0 1785288167 37728256 9097 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 9211 9097 145 145 0 9066 0
[pid=16502] vsize: 36844
Current children cumulated CPU time (s) 219.22
Current children cumulated vsize (Kb) 38968

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 9768 0 0 0 22855 63 0 0 25 0 1 0 1785288167 39243776 9471 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 9581 9471 145 145 0 9436 0
[pid=16502] vsize: 38324
Current children cumulated CPU time (s) 229.18
Current children cumulated vsize (Kb) 40448

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 10159 0 0 0 23847 66 0 0 25 0 1 0 1785288167 40833024 9862 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 9969 9862 145 145 0 9824 0
[pid=16502] vsize: 39876
Current children cumulated CPU time (s) 239.13
Current children cumulated vsize (Kb) 42000

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) T 16498 16498 6847 0 -1 0 10518 0 0 0 24841 69 0 0 25 0 1 0 1785288167 42557440 10221 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16502/statm): 10390 10221 145 145 0 10245 0
[pid=16502] vsize: 41560
Current children cumulated CPU time (s) 249.1
Current children cumulated vsize (Kb) 43684

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 10849 0 0 0 25834 71 0 0 25 0 1 0 1785288167 43900928 10552 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 10718 10552 145 145 0 10573 0
[pid=16502] vsize: 42872
Current children cumulated CPU time (s) 259.05
Current children cumulated vsize (Kb) 44996

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 11173 0 0 0 26829 73 0 0 25 0 1 0 1785288167 45219840 10876 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 11040 10876 145 145 0 10895 0
[pid=16502] vsize: 44160
Current children cumulated CPU time (s) 269.02
Current children cumulated vsize (Kb) 46284

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 11560 0 0 0 27821 76 0 0 25 0 1 0 1785288167 46792704 11263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 11424 11263 145 145 0 11279 0
[pid=16502] vsize: 45696
Current children cumulated CPU time (s) 278.97
Current children cumulated vsize (Kb) 47820

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 11922 0 0 0 28814 78 0 0 25 0 1 0 1785288167 48267264 11625 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 11784 11625 145 145 0 11639 0
[pid=16502] vsize: 47136
Current children cumulated CPU time (s) 288.92
Current children cumulated vsize (Kb) 49260

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 12242 0 0 0 29809 81 0 0 25 0 1 0 1785288167 49565696 11945 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 12101 11945 145 145 0 11956 0
[pid=16502] vsize: 48404
Current children cumulated CPU time (s) 298.9
Current children cumulated vsize (Kb) 50528

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 12585 0 0 0 30802 84 0 0 25 0 1 0 1785288167 50962432 12288 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 12442 12288 145 145 0 12297 0
[pid=16502] vsize: 49768
Current children cumulated CPU time (s) 308.86
Current children cumulated vsize (Kb) 51892

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 12952 0 0 0 31796 86 0 0 25 0 1 0 1785288167 52453376 12655 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 12806 12655 145 145 0 12661 0
[pid=16502] vsize: 51224
Current children cumulated CPU time (s) 318.82
Current children cumulated vsize (Kb) 53348

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 13407 0 0 0 32790 89 0 0 25 0 1 0 1785288167 54308864 13110 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 13259 13110 145 145 0 13114 0
[pid=16502] vsize: 53036
Current children cumulated CPU time (s) 328.79
Current children cumulated vsize (Kb) 55160

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 13834 0 0 0 33782 93 0 0 25 0 1 0 1785288167 56049664 13537 4294967295 134512640 135094434 3221224448 3221223040 134557119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 13684 13537 145 145 0 13539 0
[pid=16502] vsize: 54736
Current children cumulated CPU time (s) 338.75
Current children cumulated vsize (Kb) 56860

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 14189 0 0 0 34775 96 0 0 25 0 1 0 1785288167 57503744 13892 4294967295 134512640 135094434 3221224448 3221223120 134556538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 14039 13892 145 145 0 13894 0
[pid=16502] vsize: 56156
Current children cumulated CPU time (s) 348.71
Current children cumulated vsize (Kb) 58280

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 14477 0 0 0 35770 99 0 0 25 0 1 0 1785288167 58671104 14180 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 14324 14180 145 145 0 14179 0
[pid=16502] vsize: 57296
Current children cumulated CPU time (s) 358.69
Current children cumulated vsize (Kb) 59420

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 14730 0 0 0 36766 101 0 0 25 0 1 0 1785288167 59699200 14433 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 14575 14433 145 145 0 14430 0
[pid=16502] vsize: 58300
Current children cumulated CPU time (s) 368.67
Current children cumulated vsize (Kb) 60424

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 15000 0 0 0 37761 103 0 0 25 0 1 0 1785288167 60796928 14703 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 14843 14703 145 145 0 14698 0
[pid=16502] vsize: 59372
Current children cumulated CPU time (s) 378.64
Current children cumulated vsize (Kb) 61496

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 15300 0 0 0 38755 104 0 0 25 0 1 0 1785288167 62021632 15003 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 15142 15003 145 145 0 14997 0
[pid=16502] vsize: 60568
Current children cumulated CPU time (s) 388.59
Current children cumulated vsize (Kb) 62692

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 15528 0 0 0 39751 106 0 0 25 0 1 0 1785288167 62951424 15231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 15369 15231 145 145 0 15224 0
[pid=16502] vsize: 61476
Current children cumulated CPU time (s) 398.57
Current children cumulated vsize (Kb) 63600

[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 15861 0 0 0 40744 109 0 0 25 0 1 0 1785288167 64311296 15564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 15701 15564 145 145 0 15556 0
[pid=16502] vsize: 62804
Current children cumulated CPU time (s) 408.53
Current children cumulated vsize (Kb) 64928

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 16249 0 0 0 41737 112 0 0 25 0 1 0 1785288167 65892352 15952 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 16087 15952 145 145 0 15942 0
[pid=16502] vsize: 64348
Current children cumulated CPU time (s) 418.49
Current children cumulated vsize (Kb) 66472

[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 16550 0 0 0 42732 114 0 0 25 0 1 0 1785288167 67117056 16253 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 16386 16253 145 145 0 16241 0
[pid=16502] vsize: 65544
Current children cumulated CPU time (s) 428.46
Current children cumulated vsize (Kb) 67668

[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 16844 0 0 0 43728 115 0 0 25 0 1 0 1785288167 68313088 16547 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 16678 16547 145 145 0 16533 0
[pid=16502] vsize: 66712
Current children cumulated CPU time (s) 438.43
Current children cumulated vsize (Kb) 68836

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17119 0 0 0 44722 118 0 0 25 0 1 0 1785288167 69427200 16822 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 16950 16822 145 145 0 16805 0
[pid=16502] vsize: 67800
Current children cumulated CPU time (s) 448.4
Current children cumulated vsize (Kb) 69924

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) T 16498 16498 6847 0 -1 0 17467 0 0 0 45716 120 0 0 25 0 1 0 1785288167 70844416 17170 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17296 17170 145 145 0 17151 0
[pid=16502] vsize: 69184
Current children cumulated CPU time (s) 458.36
Current children cumulated vsize (Kb) 71308

[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 46716 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 468.36
Current children cumulated vsize (Kb) 71400

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 47717 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 478.37
Current children cumulated vsize (Kb) 71400

[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 48717 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 488.37
Current children cumulated vsize (Kb) 71400

[startup+500.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 49717 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 498.37
Current children cumulated vsize (Kb) 71400

[startup+510.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 50717 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 508.37
Current children cumulated vsize (Kb) 71400

[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 51718 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 518.38
Current children cumulated vsize (Kb) 71400

[startup+530.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 52718 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 528.38
Current children cumulated vsize (Kb) 71400

[startup+540.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 53718 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 538.38
Current children cumulated vsize (Kb) 71400

[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 54718 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 548.38
Current children cumulated vsize (Kb) 71400

[startup+560.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 55719 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 558.39
Current children cumulated vsize (Kb) 71400

[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 56719 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 568.39
Current children cumulated vsize (Kb) 71400

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 57719 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 578.39
Current children cumulated vsize (Kb) 71400

[startup+590.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 58719 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 588.39
Current children cumulated vsize (Kb) 71400

[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 59720 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 598.4
Current children cumulated vsize (Kb) 71400

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 60720 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 608.4
Current children cumulated vsize (Kb) 71400

[startup+620.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 61720 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 618.4
Current children cumulated vsize (Kb) 71400

[startup+630.059 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17490 0 0 0 62720 120 0 0 25 0 1 0 1785288167 70938624 17193 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17193 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 628.4
Current children cumulated vsize (Kb) 71400

[startup+640.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 63721 120 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 638.41
Current children cumulated vsize (Kb) 71400

[startup+650.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 64720 120 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 648.4
Current children cumulated vsize (Kb) 71400

[startup+660.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 65720 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 658.41
Current children cumulated vsize (Kb) 71400

[startup+670.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 66720 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 668.41
Current children cumulated vsize (Kb) 71400

[startup+680.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 67720 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 678.41
Current children cumulated vsize (Kb) 71400

[startup+690.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 68720 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 688.41
Current children cumulated vsize (Kb) 71400

[startup+700.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 69721 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 698.42
Current children cumulated vsize (Kb) 71400

[startup+710.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 70721 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 708.42
Current children cumulated vsize (Kb) 71400

[startup+720.069 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 71721 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 718.42
Current children cumulated vsize (Kb) 71400

[startup+730.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 72722 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 728.43
Current children cumulated vsize (Kb) 71400

[startup+740.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 73722 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 738.43
Current children cumulated vsize (Kb) 71400

[startup+750.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 74722 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223120 134555583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 748.43
Current children cumulated vsize (Kb) 71400

[startup+760.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 75722 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 758.43
Current children cumulated vsize (Kb) 71400

[startup+770.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 76722 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 768.43
Current children cumulated vsize (Kb) 71400

[startup+780.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17491 0 0 0 77723 121 0 0 25 0 1 0 1785288167 70938624 17194 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17194 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 778.44
Current children cumulated vsize (Kb) 71400

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17492 0 0 0 78723 121 0 0 25 0 1 0 1785288167 70938624 17195 4294967295 134512640 135094434 3221224448 3221223120 134556257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17195 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 788.44
Current children cumulated vsize (Kb) 71400

[startup+800.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17494 0 0 0 79723 121 0 0 25 0 1 0 1785288167 70938624 17197 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17197 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 798.44
Current children cumulated vsize (Kb) 71400

[startup+810.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17495 0 0 0 80724 121 0 0 25 0 1 0 1785288167 70938624 17198 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17198 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 808.45
Current children cumulated vsize (Kb) 71400

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17497 0 0 0 81724 121 0 0 25 0 1 0 1785288167 70938624 17200 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17319 17200 145 145 0 17174 0
[pid=16502] vsize: 69276
Current children cumulated CPU time (s) 818.45
Current children cumulated vsize (Kb) 71400

[startup+830.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17600 0 0 0 82723 121 0 0 25 0 1 0 1785288167 71364608 17303 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17423 17303 145 145 0 17278 0
[pid=16502] vsize: 69692
Current children cumulated CPU time (s) 828.44
Current children cumulated vsize (Kb) 71816

[startup+840.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17729 0 0 0 83721 122 0 0 25 0 1 0 1785288167 71892992 17432 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17552 17432 145 145 0 17407 0
[pid=16502] vsize: 70208
Current children cumulated CPU time (s) 838.43
Current children cumulated vsize (Kb) 72332

[startup+850.081 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17849 0 0 0 84719 123 0 0 25 0 1 0 1785288167 72376320 17552 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17670 17552 145 145 0 17525 0
[pid=16502] vsize: 70680
Current children cumulated CPU time (s) 848.42
Current children cumulated vsize (Kb) 72804

[startup+860.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 17977 0 0 0 85717 124 0 0 25 0 1 0 1785288167 72904704 17680 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17799 17680 145 145 0 17654 0
[pid=16502] vsize: 71196
Current children cumulated CPU time (s) 858.41
Current children cumulated vsize (Kb) 73320

[startup+870.084 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 86715 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 868.4
Current children cumulated vsize (Kb) 73744

[startup+880.085 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 87715 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 878.4
Current children cumulated vsize (Kb) 73744

[startup+890.086 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 88716 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 888.41
Current children cumulated vsize (Kb) 73744

[startup+900.086 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 89716 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 898.41
Current children cumulated vsize (Kb) 73744

[startup+910.087 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 90716 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 908.41
Current children cumulated vsize (Kb) 73744

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 91716 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 918.41
Current children cumulated vsize (Kb) 73744

[startup+930.089 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 92716 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 928.41
Current children cumulated vsize (Kb) 73744

[startup+940.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 93716 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 938.41
Current children cumulated vsize (Kb) 73744

[startup+950.091 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 94717 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223072 134557627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 948.42
Current children cumulated vsize (Kb) 73744

[startup+960.091 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 95717 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 958.42
Current children cumulated vsize (Kb) 73744

[startup+970.092 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 96717 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134558295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 968.42
Current children cumulated vsize (Kb) 73744

[startup+980.093 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 97717 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 978.42
Current children cumulated vsize (Kb) 73744

[startup+990.094 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 98717 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 988.42
Current children cumulated vsize (Kb) 73744

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 99718 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 998.43
Current children cumulated vsize (Kb) 73744

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 100718 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1008.43
Current children cumulated vsize (Kb) 73744

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 101718 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1018.43
Current children cumulated vsize (Kb) 73744

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 102718 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1028.43
Current children cumulated vsize (Kb) 73744

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 103719 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1038.44
Current children cumulated vsize (Kb) 73744

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 104719 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1048.44
Current children cumulated vsize (Kb) 73744

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 105719 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1058.44
Current children cumulated vsize (Kb) 73744

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 106719 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1068.44
Current children cumulated vsize (Kb) 73744

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 107719 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1078.44
Current children cumulated vsize (Kb) 73744

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 108720 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1088.45
Current children cumulated vsize (Kb) 73744

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 109720 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1098.45
Current children cumulated vsize (Kb) 73744

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 110720 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1108.45
Current children cumulated vsize (Kb) 73744

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 111721 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1118.46
Current children cumulated vsize (Kb) 73744

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 112721 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1128.46
Current children cumulated vsize (Kb) 73744

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18084 0 0 0 113721 125 0 0 25 0 1 0 1785288167 73338880 17787 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17787 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1138.46
Current children cumulated vsize (Kb) 73744

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18085 0 0 0 114721 125 0 0 25 0 1 0 1785288167 73338880 17788 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17788 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1148.46
Current children cumulated vsize (Kb) 73744

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18085 0 0 0 115722 125 0 0 25 0 1 0 1785288167 73338880 17788 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17788 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1158.47
Current children cumulated vsize (Kb) 73744

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18086 0 0 0 116722 125 0 0 25 0 1 0 1785288167 73338880 17789 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 17905 17789 145 145 0 17760 0
[pid=16502] vsize: 71620
Current children cumulated CPU time (s) 1168.47
Current children cumulated vsize (Kb) 73744

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18265 0 0 0 117718 127 0 0 25 0 1 0 1785288167 74072064 17968 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 18084 17968 145 145 0 17939 0
[pid=16502] vsize: 72336
Current children cumulated CPU time (s) 1178.45
Current children cumulated vsize (Kb) 74460

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18499 0 0 0 118715 128 0 0 25 0 1 0 1785288167 75042816 18202 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 18321 18202 145 145 0 18176 0
[pid=16502] vsize: 73284
Current children cumulated CPU time (s) 1188.43
Current children cumulated vsize (Kb) 75408

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 18778 0 0 0 119709 131 0 0 25 0 1 0 1785288167 76185600 18481 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 18600 18481 145 145 0 18455 0
[pid=16502] vsize: 74400
Current children cumulated CPU time (s) 1198.4
Current children cumulated vsize (Kb) 76524

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 19054 0 0 0 120705 132 0 0 25 0 1 0 1785288167 77316096 18757 4294967295 134512640 135094434 3221224448 3221223120 134556244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 18876 18757 145 145 0 18731 0
[pid=16502] vsize: 75504
Current children cumulated CPU time (s) 1208.37
Current children cumulated vsize (Kb) 77628



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 16502
Raw data (/proc/16498/stat): 16498 (minisat+_script) S 16497 16498 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785288162 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16498/statm): 531 226 485 147 0 384 0
[pid=16498] vsize: 2124
Raw data (/proc/16502/stat): 16502 (minisat+_64-bit) R 16498 16498 6847 0 -1 0 19054 0 0 0 120705 132 0 0 25 0 1 0 1785288167 77316096 18757 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16502/statm): 18876 18757 145 145 0 18731 0
[pid=16502] vsize: 75504
Current children cumulated CPU time (s) 1208.37
Current children cumulated vsize (Kb) 77628

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1208.42
CPU user time (s): 1207.06
CPU system time (s): 1.36379
CPU usage (%): 99.8569
Max. virtual memory (cumulated for all children) (Kb): 77628

Verifier Data

ERROR: no interpretation found !