Some explanations

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

General information on the benchmark

Namesubmitted/manquinho/primes-dimacs-cnf/normalized-g125.17.opb
MD5SUMed503628984a48598e5d5a4b8388e97a
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 4250
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 4250
Number of bits of the sum of numbers in the objective function 13
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 4250
Number of bits of the biggest sum of numbers13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables4250
Total number of constraints68397
Number of constraints which are clauses68397
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 constraint17

Trace number 1462

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        920356 kB
Buffers:         34196 kB
Cached:          54908 kB
SwapCached:        792 kB
Active:          65036 kB
Inactive:        26756 kB
HighTotal:      131008 kB
HighFree:        72296 kB
LowTotal:       903652 kB
LowFree:        848060 kB
SwapTotal:     2097136 kB
SwapFree:      2095876 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5752 kB
Slab:            16912 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 15:29:09 (client local time) WITH STATUS 0 IN 1206.37 SECONDS
stats: 2469 7 1206.37 0

Solver Data

c Parsing PB file...
c Converting 68397 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 |   68397   138669 |   22799       0        0     nan |  0.000 % |
c |       100 |   68397   138669 |   25078     100     5288    52.9 |  0.000 % |
c |       250 |   68397   138669 |   27586     250    27345   109.4 |  0.000 % |
c |       476 |   68397   138669 |   30345     476    55808   117.2 |  0.000 % |
c |       813 |   68397   138669 |   33380     813   105508   129.8 |  0.000 % |
c |      1319 |   68397   138669 |   36718    1319   238948   181.2 |  0.000 % |
c |      2080 |   68397   138669 |   40389    2080   408552   196.4 |  0.000 % |
c |      3220 |   68397   138669 |   44428    3220   720088   223.6 |  0.000 % |
c |      4930 |   68397   138669 |   48871    4930  1260193   255.6 |  0.000 % |
c |      7492 |   68397   138669 |   53758    7492  2077236   277.3 |  0.000 % |
c |     11336 |   68397   138669 |   59134   11336  3292984   290.5 |  0.000 % |
c |     17103 |   68397   138669 |   65048   17103  5370978   314.0 |  0.000 % |
c |     25752 |   68397   138669 |   71553   25752  8706513   338.1 |  0.000 % |
c |     38727 |   68397   138669 |   78708   38727 13018646   336.2 |  0.000 % |
c |     58190 |   68397   138669 |   86579   58190 20743435   356.5 |  0.000 % |
c |     87385 |   68397   138669 |   95237   87385 30964013   354.3 |  0.000 % |
c |    131175 |   68397   138669 |  104760   47058 17880606   380.0 |  0.000 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/950/stat): 950 (minisat+_script) R 949 950 27660 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1770426787 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/950/statm): 174 3 169 147 0 27 0
[pid=950] 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=951
New process pid=952
New process pid=953
execve syscall for /bin/sed executable
One traced child (pid=952) 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=953) exited with status: 0
One traced child (pid=951) exited with status: 0
New process pid=954
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-g125.17.opb

[startup+10.0032 s]
Raw data (loadavg): 0.52 0.72 0.88 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 4474 0 0 0 963 20 0 0 25 0 1 0 1770426792 19288064 4461 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 4709 4461 145 145 0 4564 0
[pid=954] vsize: 18836
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 20960

[startup+20.005 s]
Raw data (loadavg): 0.60 0.73 0.88 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 4730 0 0 0 1958 22 0 0 25 0 1 0 1770426792 20312064 4717 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 4959 4717 145 145 0 4814 0
[pid=954] vsize: 19836
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 21960

[startup+30.0068 s]
Raw data (loadavg): 0.66 0.74 0.88 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 6247 0 0 0 2936 30 0 0 25 0 1 0 1770426792 26525696 6234 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 6476 6234 145 145 0 6331 0
[pid=954] vsize: 25904
Current children cumulated CPU time (s) 29.67
Current children cumulated vsize (Kb) 28028

[startup+40.0076 s]
Raw data (loadavg): 0.71 0.75 0.88 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 7569 0 0 0 3915 37 0 0 25 0 1 0 1770426792 31993856 7556 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 7811 7556 145 145 0 7666 0
[pid=954] vsize: 31244
Current children cumulated CPU time (s) 39.53
Current children cumulated vsize (Kb) 33368

[startup+50.0094 s]
Raw data (loadavg): 0.75 0.75 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 8826 0 0 0 4895 47 0 0 25 0 1 0 1770426792 37126144 8813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 9064 8813 145 145 0 8919 0
[pid=954] vsize: 36256
Current children cumulated CPU time (s) 49.43
Current children cumulated vsize (Kb) 38380

[startup+60.0101 s]
Raw data (loadavg): 0.79 0.76 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 9809 0 0 0 5878 54 0 0 25 0 1 0 1770426792 41144320 9796 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 10045 9796 145 145 0 9900 0
[pid=954] vsize: 40180
Current children cumulated CPU time (s) 59.33
Current children cumulated vsize (Kb) 42304

[startup+70.0119 s]
Raw data (loadavg): 0.82 0.77 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 10565 0 0 0 6865 60 0 0 25 0 1 0 1770426792 44232704 10552 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 10799 10552 145 145 0 10654 0
[pid=954] vsize: 43196
Current children cumulated CPU time (s) 69.26
Current children cumulated vsize (Kb) 45320

[startup+80.0127 s]
Raw data (loadavg): 0.85 0.78 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 11188 0 0 0 7854 64 0 0 25 0 1 0 1770426792 46776320 11175 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 11420 11175 145 145 0 11275 0
[pid=954] vsize: 45680
Current children cumulated CPU time (s) 79.19
Current children cumulated vsize (Kb) 47804

[startup+90.0145 s]
Raw data (loadavg): 0.87 0.78 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 11806 0 0 0 8842 69 0 0 25 0 1 0 1770426792 49303552 11793 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 12037 11793 145 145 0 11892 0
[pid=954] vsize: 48148
Current children cumulated CPU time (s) 89.12
Current children cumulated vsize (Kb) 50272

[startup+100.015 s]
Raw data (loadavg): 0.89 0.79 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 12439 0 0 0 9831 74 0 0 25 0 1 0 1770426792 51888128 12426 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 12668 12426 145 145 0 12523 0
[pid=954] vsize: 50672
Current children cumulated CPU time (s) 99.06
Current children cumulated vsize (Kb) 52796

[startup+110.016 s]
Raw data (loadavg): 0.91 0.80 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 13132 0 0 0 10818 80 0 0 25 0 1 0 1770426792 54857728 13119 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 13393 13119 145 145 0 13248 0
[pid=954] vsize: 53572
Current children cumulated CPU time (s) 108.99
Current children cumulated vsize (Kb) 55696

[startup+120.018 s]
Raw data (loadavg): 0.92 0.80 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 13711 0 0 0 11806 84 0 0 25 0 1 0 1770426792 57221120 13698 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 13970 13698 145 145 0 13825 0
[pid=954] vsize: 55880
Current children cumulated CPU time (s) 118.91
Current children cumulated vsize (Kb) 58004

[startup+130.019 s]
Raw data (loadavg): 0.93 0.81 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 14299 0 0 0 12794 88 0 0 25 0 1 0 1770426792 59625472 14286 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 14557 14286 145 145 0 14412 0
[pid=954] vsize: 58228
Current children cumulated CPU time (s) 128.83
Current children cumulated vsize (Kb) 60352

[startup+140.02 s]
Raw data (loadavg): 0.94 0.81 0.89 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 14859 0 0 0 13784 92 0 0 25 0 1 0 1770426792 61915136 14846 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 15116 14846 145 145 0 14971 0
[pid=954] vsize: 60464
Current children cumulated CPU time (s) 138.77
Current children cumulated vsize (Kb) 62588

[startup+150.022 s]
Raw data (loadavg): 0.95 0.82 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 15715 0 0 0 14771 98 0 0 25 0 1 0 1770426792 65413120 15702 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 15970 15702 145 145 0 15825 0
[pid=954] vsize: 63880
Current children cumulated CPU time (s) 148.7
Current children cumulated vsize (Kb) 66004

[startup+160.023 s]
Raw data (loadavg): 0.96 0.83 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 16457 0 0 0 15758 104 0 0 25 0 1 0 1770426792 68444160 16444 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 16710 16444 145 145 0 16565 0
[pid=954] vsize: 66840
Current children cumulated CPU time (s) 158.63
Current children cumulated vsize (Kb) 68964

[startup+170.025 s]
Raw data (loadavg): 0.96 0.83 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 17117 0 0 0 16745 109 0 0 25 0 1 0 1770426792 71143424 17104 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 17369 17104 145 145 0 17224 0
[pid=954] vsize: 69476
Current children cumulated CPU time (s) 168.55
Current children cumulated vsize (Kb) 71600

[startup+180.026 s]
Raw data (loadavg): 0.97 0.84 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 17844 0 0 0 17733 114 0 0 25 0 1 0 1770426792 74113024 17831 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 18094 17831 145 145 0 17949 0
[pid=954] vsize: 72376
Current children cumulated CPU time (s) 178.48
Current children cumulated vsize (Kb) 74500

[startup+190.027 s]
Raw data (loadavg): 0.97 0.84 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 18608 0 0 0 18718 120 0 0 25 0 1 0 1770426792 77238272 18595 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 18857 18595 145 145 0 18712 0
[pid=954] vsize: 75428
Current children cumulated CPU time (s) 188.39
Current children cumulated vsize (Kb) 77552

[startup+200.028 s]
Raw data (loadavg): 0.98 0.85 0.90 1/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) T 950 950 27660 0 -1 0 19271 0 0 0 19707 124 0 0 25 0 1 0 1770426792 79953920 19258 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/954/statm): 19520 19258 145 145 0 19375 0
[pid=954] vsize: 78080
Current children cumulated CPU time (s) 198.32
Current children cumulated vsize (Kb) 80204

[startup+210.029 s]
Raw data (loadavg): 0.98 0.85 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 19966 0 0 0 20694 129 0 0 25 0 1 0 1770426792 82788352 19953 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 20212 19953 145 145 0 20067 0
[pid=954] vsize: 80848
Current children cumulated CPU time (s) 208.24
Current children cumulated vsize (Kb) 82972

[startup+220.031 s]
Raw data (loadavg): 0.98 0.85 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 20654 0 0 0 21681 135 0 0 25 0 1 0 1770426792 85602304 20641 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 20899 20641 145 145 0 20754 0
[pid=954] vsize: 83596
Current children cumulated CPU time (s) 218.17
Current children cumulated vsize (Kb) 85720

[startup+230.031 s]
Raw data (loadavg): 0.98 0.86 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 21279 0 0 0 22672 139 0 0 25 0 1 0 1770426792 88170496 21266 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 21526 21266 145 145 0 21381 0
[pid=954] vsize: 86104
Current children cumulated CPU time (s) 228.12
Current children cumulated vsize (Kb) 88228

[startup+240.033 s]
Raw data (loadavg): 0.99 0.86 0.90 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 21936 0 0 0 23661 144 0 0 25 0 1 0 1770426792 90845184 21923 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 22179 21923 145 145 0 22034 0
[pid=954] vsize: 88716
Current children cumulated CPU time (s) 238.06
Current children cumulated vsize (Kb) 90840

[startup+250.034 s]
Raw data (loadavg): 0.99 0.87 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 22626 0 0 0 24648 150 0 0 25 0 1 0 1770426792 93663232 22613 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 22867 22613 145 145 0 22722 0
[pid=954] vsize: 91468
Current children cumulated CPU time (s) 247.99
Current children cumulated vsize (Kb) 93592

[startup+260.035 s]
Raw data (loadavg): 0.99 0.87 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 23249 0 0 0 25636 155 0 0 25 0 1 0 1770426792 96206848 23236 4294967295 134512640 135094434 3221224448 3221223040 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 23488 23236 145 145 0 23343 0
[pid=954] vsize: 93952
Current children cumulated CPU time (s) 257.92
Current children cumulated vsize (Kb) 96076

[startup+270.037 s]
Raw data (loadavg): 0.99 0.87 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 23828 0 0 0 26626 159 0 0 25 0 1 0 1770426792 98574336 23815 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 24066 23815 145 145 0 23921 0
[pid=954] vsize: 96264
Current children cumulated CPU time (s) 267.86
Current children cumulated vsize (Kb) 98388

[startup+280.037 s]
Raw data (loadavg): 0.99 0.88 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 24317 0 0 0 27616 163 0 0 25 0 1 0 1770426792 100577280 24304 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 24555 24304 145 145 0 24410 0
[pid=954] vsize: 98220
Current children cumulated CPU time (s) 277.8
Current children cumulated vsize (Kb) 100344

[startup+290.039 s]
Raw data (loadavg): 0.99 0.88 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 24909 0 0 0 28606 168 0 0 25 0 1 0 1770426792 102993920 24896 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 25145 24896 145 145 0 25000 0
[pid=954] vsize: 100580
Current children cumulated CPU time (s) 287.75
Current children cumulated vsize (Kb) 102704

[startup+300.04 s]
Raw data (loadavg): 0.99 0.89 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 25506 0 0 0 29595 172 0 0 25 0 1 0 1770426792 105697280 25493 4294967295 134512640 135094434 3221224448 3221223096 134557061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 25805 25493 145 145 0 25660 0
[pid=954] vsize: 103220
Current children cumulated CPU time (s) 297.68
Current children cumulated vsize (Kb) 105344

[startup+310.041 s]
Raw data (loadavg): 0.99 0.89 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 26094 0 0 0 30585 176 0 0 25 0 1 0 1770426792 108101632 26081 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 26392 26081 145 145 0 26247 0
[pid=954] vsize: 105568
Current children cumulated CPU time (s) 307.62
Current children cumulated vsize (Kb) 107692

[startup+320.041 s]
Raw data (loadavg): 0.99 0.89 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 26683 0 0 0 31576 180 0 0 25 0 1 0 1770426792 110530560 26670 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 26985 26670 145 145 0 26840 0
[pid=954] vsize: 107940
Current children cumulated CPU time (s) 317.57
Current children cumulated vsize (Kb) 110064

[startup+330.043 s]
Raw data (loadavg): 0.99 0.89 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 27149 0 0 0 32568 183 0 0 25 0 1 0 1770426792 112435200 27136 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 27450 27136 145 145 0 27305 0
[pid=954] vsize: 109800
Current children cumulated CPU time (s) 327.52
Current children cumulated vsize (Kb) 111924

[startup+340.044 s]
Raw data (loadavg): 0.99 0.90 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 27663 0 0 0 33557 187 0 0 25 0 1 0 1770426792 114544640 27650 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 27965 27650 145 145 0 27820 0
[pid=954] vsize: 111860
Current children cumulated CPU time (s) 337.45
Current children cumulated vsize (Kb) 113984

[startup+350.045 s]
Raw data (loadavg): 0.99 0.90 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 28206 0 0 0 34547 190 0 0 25 0 1 0 1770426792 116764672 28193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 28507 28193 145 145 0 28362 0
[pid=954] vsize: 114028
Current children cumulated CPU time (s) 347.38
Current children cumulated vsize (Kb) 116152

[startup+360.046 s]
Raw data (loadavg): 0.99 0.90 0.91 1/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) T 950 950 27660 0 -1 0 28755 0 0 0 35537 195 0 0 25 0 1 0 1770426792 119005184 28742 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/954/statm): 29054 28742 145 145 0 28909 0
[pid=954] vsize: 116216
Current children cumulated CPU time (s) 357.33
Current children cumulated vsize (Kb) 118340

[startup+370.046 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 29225 0 0 0 36526 198 0 0 25 0 1 0 1770426792 120942592 29212 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 29527 29212 145 145 0 29382 0
[pid=954] vsize: 118108
Current children cumulated CPU time (s) 367.25
Current children cumulated vsize (Kb) 120232

[startup+380.047 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 29720 0 0 0 37517 202 0 0 25 0 1 0 1770426792 122970112 29707 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 30022 29707 145 145 0 29877 0
[pid=954] vsize: 120088
Current children cumulated CPU time (s) 377.2
Current children cumulated vsize (Kb) 122212

[startup+390.049 s]
Raw data (loadavg): 0.99 0.91 0.91 1/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) T 950 950 27660 0 -1 0 30241 0 0 0 38508 205 0 0 25 0 1 0 1770426792 125104128 30228 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/954/statm): 30543 30228 145 145 0 30398 0
[pid=954] vsize: 122172
Current children cumulated CPU time (s) 387.14
Current children cumulated vsize (Kb) 124296

[startup+400.05 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 30591 0 0 0 39503 208 0 0 25 0 1 0 1770426792 126537728 30578 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 30893 30578 145 145 0 30748 0
[pid=954] vsize: 123572
Current children cumulated CPU time (s) 397.12
Current children cumulated vsize (Kb) 125696

[startup+410.05 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) T 950 950 27660 0 -1 0 30987 0 0 0 40496 210 0 0 25 0 1 0 1770426792 128159744 30974 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/954/statm): 31289 30974 145 145 0 31144 0
[pid=954] vsize: 125156
Current children cumulated CPU time (s) 407.07
Current children cumulated vsize (Kb) 127280

[startup+420.05 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 31398 0 0 0 41489 214 0 0 25 0 1 0 1770426792 129839104 31385 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 31699 31385 145 145 0 31554 0
[pid=954] vsize: 126796
Current children cumulated CPU time (s) 417.04
Current children cumulated vsize (Kb) 128920

[startup+430.051 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 31746 0 0 0 42484 215 0 0 25 0 1 0 1770426792 131264512 31733 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 32047 31733 145 145 0 31902 0
[pid=954] vsize: 128188
Current children cumulated CPU time (s) 427
Current children cumulated vsize (Kb) 130312

[startup+440.052 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 32036 0 0 0 43479 218 0 0 25 0 1 0 1770426792 132456448 32023 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 32338 32023 145 145 0 32193 0
[pid=954] vsize: 129352
Current children cumulated CPU time (s) 436.98
Current children cumulated vsize (Kb) 131476

[startup+450.053 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 32352 0 0 0 44474 219 0 0 25 0 1 0 1770426792 133746688 32339 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 32653 32339 145 145 0 32508 0
[pid=954] vsize: 130612
Current children cumulated CPU time (s) 446.94
Current children cumulated vsize (Kb) 132736

[startup+460.052 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 32624 0 0 0 45469 221 0 0 25 0 1 0 1770426792 134877184 32611 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 32929 32611 145 145 0 32784 0
[pid=954] vsize: 131716
Current children cumulated CPU time (s) 456.91
Current children cumulated vsize (Kb) 133840

[startup+470.053 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 32893 0 0 0 46465 223 0 0 25 0 1 0 1770426792 135983104 32880 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 33199 32880 145 145 0 33054 0
[pid=954] vsize: 132796
Current children cumulated CPU time (s) 466.89
Current children cumulated vsize (Kb) 134920

[startup+480.054 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 33153 0 0 0 47461 225 0 0 25 0 1 0 1770426792 137048064 33140 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 33459 33140 145 145 0 33314 0
[pid=954] vsize: 133836
Current children cumulated CPU time (s) 476.87
Current children cumulated vsize (Kb) 135960

[startup+490.055 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 33558 0 0 0 48453 229 0 0 25 0 1 0 1770426792 138719232 33545 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 33867 33545 145 145 0 33722 0
[pid=954] vsize: 135468
Current children cumulated CPU time (s) 486.83
Current children cumulated vsize (Kb) 137592

[startup+500.056 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 33906 0 0 0 49446 232 0 0 25 0 1 0 1770426792 140152832 33893 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 34217 33893 145 145 0 34072 0
[pid=954] vsize: 136868
Current children cumulated CPU time (s) 496.79
Current children cumulated vsize (Kb) 138992

[startup+510.056 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 34262 0 0 0 50438 236 0 0 25 0 1 0 1770426792 141615104 34249 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 34574 34249 145 145 0 34429 0
[pid=954] vsize: 138296
Current children cumulated CPU time (s) 506.75
Current children cumulated vsize (Kb) 140420

[startup+520.057 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 34687 0 0 0 51431 239 0 0 25 0 1 0 1770426792 143347712 34674 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 34997 34674 145 145 0 34852 0
[pid=954] vsize: 139988
Current children cumulated CPU time (s) 516.71
Current children cumulated vsize (Kb) 142112

[startup+530.058 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 35111 0 0 0 52422 243 0 0 25 0 1 0 1770426792 145080320 35098 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 35420 35098 145 145 0 35275 0
[pid=954] vsize: 141680
Current children cumulated CPU time (s) 526.66
Current children cumulated vsize (Kb) 143804

[startup+540.06 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 35483 0 0 0 53413 248 0 0 25 0 1 0 1770426792 146604032 35470 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 35792 35470 145 145 0 35647 0
[pid=954] vsize: 143168
Current children cumulated CPU time (s) 536.62
Current children cumulated vsize (Kb) 145292

[startup+550.061 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 35881 0 0 0 54405 252 0 0 25 0 1 0 1770426792 148238336 35868 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 36191 35868 145 145 0 36046 0
[pid=954] vsize: 144764
Current children cumulated CPU time (s) 546.58
Current children cumulated vsize (Kb) 146888

[startup+560.061 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 36294 0 0 0 55396 256 0 0 25 0 1 0 1770426792 149938176 36281 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 36606 36281 145 145 0 36461 0
[pid=954] vsize: 146424
Current children cumulated CPU time (s) 556.53
Current children cumulated vsize (Kb) 148548

[startup+570.063 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 36735 0 0 0 56389 259 0 0 25 0 1 0 1770426792 151744512 36722 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37047 36722 145 145 0 36902 0
[pid=954] vsize: 148188
Current children cumulated CPU time (s) 566.49
Current children cumulated vsize (Kb) 150312

[startup+580.064 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37086 0 0 0 57382 263 0 0 25 0 1 0 1770426792 153186304 37073 4294967295 134512640 135094434 3221224448 3221223040 134551718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37399 37073 145 145 0 37254 0
[pid=954] vsize: 149596
Current children cumulated CPU time (s) 576.46
Current children cumulated vsize (Kb) 151720

[startup+590.065 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37229 0 0 0 58379 264 0 0 25 0 1 0 1770426792 153767936 37216 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37216 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 586.44
Current children cumulated vsize (Kb) 152288

[startup+600.066 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37229 0 0 0 59378 265 0 0 25 0 1 0 1770426792 153767936 37216 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37216 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 596.44
Current children cumulated vsize (Kb) 152288

[startup+610.067 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37229 0 0 0 60378 265 0 0 25 0 1 0 1770426792 153767936 37216 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37216 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 606.44
Current children cumulated vsize (Kb) 152288

[startup+620.068 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37229 0 0 0 61378 265 0 0 25 0 1 0 1770426792 153767936 37216 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37216 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 616.44
Current children cumulated vsize (Kb) 152288

[startup+630.07 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 62378 265 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 626.44
Current children cumulated vsize (Kb) 152288

[startup+640.071 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 63377 266 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 636.44
Current children cumulated vsize (Kb) 152288

[startup+650.071 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 64377 266 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 646.44
Current children cumulated vsize (Kb) 152288

[startup+660.072 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 65377 267 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223080 134557563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 656.45
Current children cumulated vsize (Kb) 152288

[startup+670.074 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 66376 267 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 666.44
Current children cumulated vsize (Kb) 152288

[startup+680.075 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 67376 268 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 676.45
Current children cumulated vsize (Kb) 152288

[startup+690.076 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 68376 268 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 686.45
Current children cumulated vsize (Kb) 152288

[startup+700.076 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37231 0 0 0 69375 268 0 0 25 0 1 0 1770426792 153767936 37218 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37218 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 696.44
Current children cumulated vsize (Kb) 152288

[startup+710.077 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37232 0 0 0 70375 268 0 0 25 0 1 0 1770426792 153767936 37219 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37219 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 706.44
Current children cumulated vsize (Kb) 152288

[startup+720.079 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 71375 269 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 716.45
Current children cumulated vsize (Kb) 152288

[startup+730.08 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 72375 269 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 726.45
Current children cumulated vsize (Kb) 152288

[startup+740.079 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 73374 269 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 736.44
Current children cumulated vsize (Kb) 152288

[startup+750.081 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 74374 270 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 746.45
Current children cumulated vsize (Kb) 152288

[startup+760.082 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 75373 270 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 756.44
Current children cumulated vsize (Kb) 152288

[startup+770.084 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 76373 270 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 766.44
Current children cumulated vsize (Kb) 152288

[startup+780.085 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 77373 271 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 776.45
Current children cumulated vsize (Kb) 152288

[startup+790.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 78372 271 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 786.44
Current children cumulated vsize (Kb) 152288

[startup+800.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 79372 272 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 796.45
Current children cumulated vsize (Kb) 152288

[startup+810.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 80371 272 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 806.44
Current children cumulated vsize (Kb) 152288

[startup+820.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 81371 272 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 816.44
Current children cumulated vsize (Kb) 152288

[startup+830.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 82370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 826.44
Current children cumulated vsize (Kb) 152288

[startup+840.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 83370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 836.44
Current children cumulated vsize (Kb) 152288

[startup+850.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 84370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 846.44
Current children cumulated vsize (Kb) 152288

[startup+860.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 85370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 856.44
Current children cumulated vsize (Kb) 152288

[startup+870.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 86370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 866.44
Current children cumulated vsize (Kb) 152288

[startup+880.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 87370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 876.44
Current children cumulated vsize (Kb) 152288

[startup+890.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 88370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 886.44
Current children cumulated vsize (Kb) 152288

[startup+900.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 89371 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 896.45
Current children cumulated vsize (Kb) 152288

[startup+910.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 90371 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 906.45
Current children cumulated vsize (Kb) 152288

[startup+920.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 91371 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 916.45
Current children cumulated vsize (Kb) 152288

[startup+930.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 92371 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 926.45
Current children cumulated vsize (Kb) 152288

[startup+940.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 93372 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 936.46
Current children cumulated vsize (Kb) 152288

[startup+950.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 94372 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 946.46
Current children cumulated vsize (Kb) 152288

[startup+960.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 95372 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223040 134556715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 956.46
Current children cumulated vsize (Kb) 152288

[startup+970.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 96372 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 966.46
Current children cumulated vsize (Kb) 152288

[startup+980.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 97373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 976.47
Current children cumulated vsize (Kb) 152288

[startup+990.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 98373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 986.47
Current children cumulated vsize (Kb) 152288

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 99373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 996.47
Current children cumulated vsize (Kb) 152288

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 100373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1006.47
Current children cumulated vsize (Kb) 152288

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 101373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1016.47
Current children cumulated vsize (Kb) 152288

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 102374 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1026.48
Current children cumulated vsize (Kb) 152288

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 103374 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1036.48
Current children cumulated vsize (Kb) 152288

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 104374 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1046.48
Current children cumulated vsize (Kb) 152288

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 105374 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1056.48
Current children cumulated vsize (Kb) 152288

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 106375 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1066.49
Current children cumulated vsize (Kb) 152288

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 107375 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1076.49
Current children cumulated vsize (Kb) 152288

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 108375 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1086.49
Current children cumulated vsize (Kb) 152288

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 109375 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1096.49
Current children cumulated vsize (Kb) 152288

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 110376 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1106.5
Current children cumulated vsize (Kb) 152288

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 111376 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1116.5
Current children cumulated vsize (Kb) 152288

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 112376 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1126.5
Current children cumulated vsize (Kb) 152288

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 113376 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1136.5
Current children cumulated vsize (Kb) 152288

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 114377 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0
[pid=954] vsize: 150164
Current children cumulated CPU time (s) 1146.51
Current children cumulated vsize (Kb) 152288

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37292 0 0 0 115376 274 0 0 25 0 1 0 1770426792 154005504 37279 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37599 37279 145 145 0 37454 0
[pid=954] vsize: 150396
Current children cumulated CPU time (s) 1156.51
Current children cumulated vsize (Kb) 152520

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37667 0 0 0 116368 278 0 0 25 0 1 0 1770426792 155541504 37654 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 37974 37654 145 145 0 37829 0
[pid=954] vsize: 151896
Current children cumulated CPU time (s) 1166.47
Current children cumulated vsize (Kb) 154020

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 38129 0 0 0 117361 282 0 0 25 0 1 0 1770426792 157433856 38116 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 38436 38116 145 145 0 38291 0
[pid=954] vsize: 153744
Current children cumulated CPU time (s) 1176.44
Current children cumulated vsize (Kb) 155868

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 38554 0 0 0 118352 285 0 0 25 0 1 0 1770426792 159174656 38541 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 38861 38541 145 145 0 38716 0
[pid=954] vsize: 155444
Current children cumulated CPU time (s) 1186.38
Current children cumulated vsize (Kb) 157568

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 39021 0 0 0 119346 287 0 0 25 0 1 0 1770426792 161091584 39008 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 39329 39008 145 145 0 39184 0
[pid=954] vsize: 157316
Current children cumulated CPU time (s) 1196.34
Current children cumulated vsize (Kb) 159440

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 39447 0 0 0 120338 290 0 0 25 0 1 0 1770426792 162840576 39434 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 39756 39434 145 145 0 39611 0
[pid=954] vsize: 159024
Current children cumulated CPU time (s) 1206.29
Current children cumulated vsize (Kb) 161148



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 954
Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/950/statm): 531 226 485 147 0 384 0
[pid=950] vsize: 2124
Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 39447 0 0 0 120338 290 0 0 25 0 1 0 1770426792 162840576 39434 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/954/statm): 39756 39434 145 145 0 39611 0
[pid=954] vsize: 159024
Current children cumulated CPU time (s) 1206.29
Current children cumulated vsize (Kb) 161148

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1206.37
CPU user time (s): 1203.39
CPU system time (s): 2.98255
CPU usage (%): 99.6841
Max. virtual memory (cumulated for all children) (Kb): 161148

Verifier Data

ERROR: no interpretation found !