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).
  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

Namenormalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-3.opb
MD5SUM140696e76e8ed6af142b84a22a9a8f01
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -38
Optimality of the best value was proved NO
Number of terms in the objective function 1150
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 1150
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1150
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.09
Number of variables1150
Total number of constraints81068
Number of constraints which are clauses81068
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 5630

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 01:03:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4096 boxname=wulflinc21 idbench=336 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  140696e76e8ed6af142b84a22a9a8f01  /oldhome/oroussel/tmp/wulflinc21/normalized-frb50-23-3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-frb50-23-3.opb /oldhome/oroussel/tmp/wulflinc21/normalized-frb50-23-3.opb
IDLAUNCH: 4096
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        878296 kB
Buffers:         27476 kB
Cached:         108456 kB
SwapCached:          0 kB
Active:          36204 kB
Inactive:       102632 kB
HighTotal:      131008 kB
HighFree:        18900 kB
LowTotal:       903652 kB
LowFree:        859396 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11900 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:23:47 (client local time) WITH STATUS 10 IN 1209.81 SECONDS
stats: 4096 7 1209.81 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 81068 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   81068   162136 |   24320       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   81068   162136 |   32427       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.30234 s)
c ==============================================================================
c Found solution: -34
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  148830   321097 |   44648       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/46117          
c   -- var.elim.:  2000/46117          
c   -- var.elim.:  3000/46117          
c   -- var.elim.:  4000/46117          
c   -- var.elim.:  5000/46117          
c   -- var.elim.:  6000/46117          
c   -- var.elim.:  7000/46117          
c   -- var.elim.:  8000/46117          
c   -- var.elim.:  9000/46117          
c   -- var.elim.:  10000/46117          
c   -- var.elim.:  11000/46117          
c   -- var.elim.:  12000/46117          
c   -- var.elim.:  13000/46117          
c   -- var.elim.:  14000/46117          
c   -- var.elim.:  15000/46117          
c   -- var.elim.:  16000/46117          
c   -- var.elim.:  17000/46117          
c   -- var.elim.:  18000/46117          
c   -- var.elim.:  19000/46117          
c   -- var.elim.:  20000/46117          
c   -- var.elim.:  21000/46117          
c   -- var.elim.:  22000/46117          
c   -- var.elim.:  23000/46117          
c   -- var.elim.:  24000/46117          
c   -- var.elim.:  25000/46117          
c   -- var.elim.:  26000/46117          
c   -- var.elim.:  27000/46117          
c   -- var.elim.:  28000/46117          
c   -- var.elim.:  29000/46117          
c   -- var.elim.:  30000/46117          
c   -- var.elim.:  31000/46117          
c   -- var.elim.:  32000/46117          
c   -- var.elim.:  33000/46117          
c   -- var.elim.:  34000/46117          
c   -- var.elim.:  35000/46117          
c   -- var.elim.:  36000/46117          
c   -- var.elim.:  37000/46117          
c   -- var.elim.:  38000/46117          
c   -- var.elim.:  39000/46117          
c   -- var.elim.:  40000/46117          
c   -- var.elim.:  41000/46117          
c   -- var.elim.:  42000/46117          
c   -- var.elim.:  43000/46117          
c   -- var.elim.:  44000/46117          
c   -- var.elim.:  45000/46117          
c   -- var.elim.:  46000/46117          
c   -- var.elim.:  46117/46117          
c   -- var.elim.:  1000/23378          
c   -- var.elim.:  2000/23378          
c   -- var.elim.:  3000/23378          
c   -- var.elim.:  4000/23378          
c   -- var.elim.:  5000/23378          
c   -- var.elim.:  6000/23378          
c   -- var.elim.:  7000/23378          
c   -- var.elim.:  8000/23378          
c   -- var.elim.:  9000/23378          
c   -- var.elim.:  10000/23378          
c   -- var.elim.:  11000/23378          
c   -- var.elim.:  12000/23378          
c   -- var.elim.:  13000/23378          
c   -- var.elim.:  14000/23378          
c   -- var.elim.:  15000/23378          
c   -- var.elim.:  16000/23378          
c   -- var.elim.:  17000/23378          
c   -- var.elim.:  18000/23378          
c   -- var.elim.:  19000/23378          
c   -- var.elim.:  20000/23378          
c   -- var.elim.:  21000/23378          
c   -- var.elim.:  22000/23378          
c   -- var.elim.:  23000/23378          
c   -- var.elim.:  23378/23378          
c   -- var.elim.:  195/195          
c   -- var.elim.:  108/108          
c   -- subsuming                       
c   -- var.elim.:  1000/9152          
c   -- var.elim.:  2000/9152          
c   -- var.elim.:  3000/9152          
c   -- var.elim.:  4000/9152          
c   -- var.elim.:  5000/9152          
c   -- var.elim.:  6000/9152          
c   -- var.elim.:  7000/9152          
c   -- var.elim.:  8000/9152          
c   -- var.elim.:  9000/9152          
c   -- var.elim.:  9152/9152          
c   -- var.elim.:  303/303          
c |         0 |  100892   340188 |      --       0       --      -- |     --   | -47932/19109
c |         0 |  100892   340188 |   40356       0        0     nan |  0.000 % |
c |       101 |  100892   340188 |   44392     101    12083   119.6 | 53.747 % |
c |       251 |  100892   340188 |   48831     251    35097   139.8 | 53.747 % |
c |       476 |  100892   340188 |   53714     476   100999   212.2 | 53.747 % |
c |       813 |  100892   340188 |   59086     813   171228   210.6 | 53.747 % |
c |      1319 |  100892   340188 |   64995    1319   271760   206.0 | 53.747 % |
c |      2078 |  100892   340188 |   71494    2078   384347   185.0 | 53.747 % |
c |      3217 |  100892   340188 |   78643    3217   617334   191.9 | 53.747 % |
c |      4925 |  100892   340188 |   86508    4925  1049314   213.1 | 53.747 % |
c ==============================================================================
c (current CPU-time: 307.105 s)
c ==============================================================================
c Found solution: -36
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6025 |  111239   368545 |   33371    6025  1316312   218.5 | 53.747 % |
c   -- subsuming                       
c   -- var.elim.:  1000/17884          
c   -- var.elim.:  2000/17884          
c   -- var.elim.:  3000/17884          
c   -- var.elim.:  4000/17884          
c   -- var.elim.:  5000/17884          
c   -- var.elim.:  6000/17884          
c   -- var.elim.:  7000/17884          
c   -- var.elim.:  8000/17884          
c   -- var.elim.:  9000/17884          
c   -- var.elim.:  10000/17884          
c   -- var.elim.:  11000/17884          
c   -- var.elim.:  12000/17884          
c   -- var.elim.:  13000/17884          
c   -- var.elim.:  14000/17884          
c   -- var.elim.:  15000/17884          
c   -- var.elim.:  16000/17884          
c   -- var.elim.:  17000/17884          
c   -- var.elim.:  17884/17884          
c   -- var.elim.:  1000/7671          
c   -- var.elim.:  2000/7671          
c   -- var.elim.:  3000/7671          
c   -- var.elim.:  4000/7671          
c   -- var.elim.:  5000/7671          
c   -- var.elim.:  6000/7671          
c   -- var.elim.:  7000/7671          
c   -- var.elim.:  7671/7671          
c   -- var.elim.:  222/222          
c   -- subsuming                       
c   -- var.elim.:  1000/6351          
c   -- var.elim.:  2000/6351          
c   -- var.elim.:  3000/6351          
c   -- var.elim.:  4000/6351          
c   -- var.elim.:  5000/6351          
c   -- var.elim.:  6000/6351          
c   -- var.elim.:  6351/6351          
c   -- var.elim.:  94/94          
c |      6025 |  101008   348080 |      --    6025       --      -- |     --   | -10214/-18482
c |      6025 |  101008   348080 |   40403    5721  1059944   185.3 | 53.747 % |
c |      6125 |  101008   348080 |   44443    5821  1079767   185.5 | 60.946 % |
c |      6275 |  101008   348080 |   48887    5971  1138903   190.7 | 60.946 % |
c |      6500 |  101008   348080 |   53776    6196  1194916   192.9 | 60.946 % |
c |      6837 |  100964   347593 |   59128    6527  1273665   195.1 | 61.025 % |
c |      7343 |  100942   347338 |   65027    7026  1382454   196.8 | 61.065 % |
c |      8102 |  100761   345466 |   71401    7777  1559752   200.6 | 61.353 % |
c |      9243 |  100725   345072 |   78513    8913  1845029   207.0 | 61.415 % |
c |     10951 |  100506   342970 |   86177   10612  2251481   212.2 | 61.776 % |
c |     13513 |  100506   342970 |   94795   13174  3141932   238.5 | 61.776 % |
c |     17357 |  100329   341231 |  104091   16997  4564597   268.6 | 62.075 % |
c |     23123 |   99556   333573 |  113617   22665  6585902   290.6 | 63.389 % |
c ==============================================================================
c (current CPU-time: 464.324 s)
c ==============================================================================
c Found solution: -38
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26253 |  101332   336479 |   30399   25760  7828826   303.9 | 63.389 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11347          
c   -- var.elim.:  2000/11347          
c   -- var.elim.:  3000/11347          
c   -- var.elim.:  4000/11347          
c   -- var.elim.:  5000/11347          
c   -- var.elim.:  6000/11347          
c   -- var.elim.:  7000/11347          
c   -- var.elim.:  8000/11347          
c   -- var.elim.:  9000/11347          
c   -- var.elim.:  10000/11347          
c   -- var.elim.:  11000/11347          
c   -- var.elim.:  11347/11347          
c   -- var.elim.:  1000/3323          
c   -- var.elim.:  2000/3323          
c   -- var.elim.:  3000/3323          
c   -- var.elim.:  3323/3323          
c   -- var.elim.:  185/185          
c |     26253 |   99308   328484 |      --   25760       --      -- |     --   | -2007/538
c |     26253 |   99308   328484 |   39723   23860  4766544   199.8 | 63.389 % |
c ==============================================================================
c (current CPU-time: 492.396 s)
c ==============================================================================
c Found solution: -39
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26349 |  108635   353735 |   32590   23956  4817658   201.1 | 63.389 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15825          
c   -- var.elim.:  2000/15825          
c   -- var.elim.:  3000/15825          
c   -- var.elim.:  4000/15825          
c   -- var.elim.:  5000/15825          
c   -- var.elim.:  6000/15825          
c   -- var.elim.:  7000/15825          
c   -- var.elim.:  8000/15825          
c   -- var.elim.:  9000/15825          
c   -- var.elim.:  10000/15825          
c   -- var.elim.:  11000/15825          
c   -- var.elim.:  12000/15825          
c   -- var.elim.:  13000/15825          
c   -- var.elim.:  14000/15825          
c   -- var.elim.:  15000/15825          
c   -- var.elim.:  15825/15825          
c   -- var.elim.:  1000/6594          
c   -- var.elim.:  2000/6594          
c   -- var.elim.:  3000/6594          
c   -- var.elim.:  4000/6594          
c   -- var.elim.:  5000/6594          
c   -- var.elim.:  6000/6594          
c   -- var.elim.:  6594/6594          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  1000/6354          
c   -- var.elim.:  2000/6354          
c   -- var.elim.:  3000/6354          
c   -- var.elim.:  4000/6354          
c   -- var.elim.:  5000/6354          
c   -- var.elim.:  6000/6354          
c   -- var.elim.:  6354/6354          
c   -- var.elim.:  17/17          
c |     26349 |   99432   338231 |      --   23956       --      -- |     --   | -9195/-15487
c |     26349 |   99432   338231 |   39772   23956  4817658   201.1 | 63.389 % |
c |     26451 |   99432   338231 |   43750   24058  4836397   201.0 | 64.966 % |
c |     26601 |   99432   338231 |   48125   24208  4899663   202.4 | 64.966 % |
c |     26826 |   99432   338231 |   52937   24433  4947565   202.5 | 64.966 % |
c |     27163 |   99368   337768 |   58193   24535  4980443   203.0 | 65.046 % |
c |     27669 |   99368   337768 |   64013   25041  5139272   205.2 | 65.046 % |
c |     28429 |   99368   337768 |   70414   25801  5410376   209.7 | 65.046 % |
c |     29568 |   99248   336626 |   77362   26930  5706240   211.9 | 65.255 % |
c |     31276 |   99154   335654 |   85018   28607  6222488   217.5 | 65.419 % |
c ==============================================================================
c (current CPU-time: 588.496 s)
c ==============================================================================
c Found solution: -41
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     32594 |   99393   335337 |   29817   29909  6644875   222.2 | 65.419 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8466          
c   -- var.elim.:  2000/8466          
c   -- var.elim.:  3000/8466          
c   -- var.elim.:  4000/8466          
c   -- var.elim.:  5000/8466          
c   -- var.elim.:  6000/8466          
c   -- var.elim.:  7000/8466          
c   -- var.elim.:  8000/8466          
c   -- var.elim.:  8466/8466          
c   -- var.elim.:  356/356          
c   -- var.elim.:  3/3          
c |     32594 |   99038   334813 |      --   29909       --      -- |     --   | -355/-523
c |     32594 |   99038   334813 |   39615   29909  6644875   222.2 | 65.419 % |
c |     32695 |   99038   334813 |   43576   30010  6678002   222.5 | 65.657 % |
c |     32845 |   98970   334150 |   47901   30082  6681152   222.1 | 65.775 % |
c |     33070 |   98970   334150 |   52691   30307  6763666   223.2 | 65.775 % |
c |     33407 |   98950   333928 |   57949   30632  6869049   224.2 | 65.810 % |
c |     33913 |   98874   333160 |   63695   31129  7042506   226.2 | 65.943 % |
c |     34672 |   98806   332533 |   70016   31866  7379338   231.6 | 66.061 % |
c |     35811 |   98690   331374 |   76927   32984  7732134   234.4 | 66.263 % |
c |     37520 |   98630   330797 |   84568   34666  8227094   237.3 | 66.368 % |
c |     40082 |   98512   329689 |   92914   37214  9091264   244.3 | 66.570 % |
c |     43926 |   98401   328551 |  102090   41026 10483329   255.5 | 66.762 % |
c |     49692 |   98107   325728 |  111964   46737 12778050   273.4 | 67.275 % |
c |     58341 |   97257   317290 |  122093   55201 15929869   288.6 | 68.725 % |
c |     71315 |   96909   313817 |  133822   68091 21048572   309.1 | 69.315 % |
c |     90776 |   95797   302642 |  145515   87304 29247279   335.0 | 71.211 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 C601 -C600 -C599 -C598 -C597 C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 C331 -C330 -C329 -C328 -C327 -C326 -C#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 1.28 1.04 0.93 2/55 3122
Raw data (stat): 3122 (runsolver) R 3121 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 357746392 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 1.24 1.03 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9373 0 0 0 955 44 0 0 25 0 1 0 357746392 41185280 8795 4294967295 134512640 134672761 3221224560 3221222864 134566562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8795 603 41 0 10014 0
vsize: 40220
[startup+20.001 s]
Raw data (loadavg): 1.20 1.03 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9374 0 0 0 1954 44 0 0 25 0 1 0 357746392 41185280 8796 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10055 8796 603 41 0 10014 0
vsize: 40220
[startup+30.0021 s]
Raw data (loadavg): 1.17 1.03 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9381 0 0 0 2955 44 0 0 25 0 1 0 357746392 41185280 8803 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8803 603 41 0 10014 0
vsize: 40220
[startup+40.0023 s]
Raw data (loadavg): 1.14 1.03 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9381 0 0 0 3954 44 0 0 25 0 1 0 357746392 41185280 8803 4294967295 134512640 134672761 3221224560 3221223152 134607938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8803 603 41 0 10014 0
vsize: 40220
[startup+50.002 s]
Raw data (loadavg): 1.12 1.03 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9382 0 0 0 4954 44 0 0 25 0 1 0 357746392 41185280 8804 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8804 603 41 0 10014 0
vsize: 40220
[startup+60.0027 s]
Raw data (loadavg): 1.10 1.03 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9383 0 0 0 5954 44 0 0 25 0 1 0 357746392 41185280 8805 4294967295 134512640 134672761 3221224560 3221222992 134604055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8805 603 41 0 10014 0
vsize: 40220
[startup+70.0034 s]
Raw data (loadavg): 1.09 1.03 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9384 0 0 0 6955 44 0 0 25 0 1 0 357746392 41185280 8806 4294967295 134512640 134672761 3221224560 3221223056 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8806 603 41 0 10014 0
vsize: 40220
[startup+80.0041 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9390 0 0 0 7955 45 0 0 25 0 1 0 357746392 41185280 8812 4294967295 134512640 134672761 3221224560 3221222992 134605675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8812 603 41 0 10014 0
vsize: 40220
[startup+90.0042 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9391 0 0 0 8954 45 0 0 25 0 1 0 357746392 41185280 8813 4294967295 134512640 134672761 3221224560 3221222880 1075352369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8813 603 41 0 10014 0
vsize: 40220
[startup+100.003 s]
Raw data (loadavg): 1.05 1.02 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9395 0 0 0 9954 45 0 0 25 0 1 0 357746392 41349120 8817 4294967295 134512640 134672761 3221224560 3221223040 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10095 8817 603 41 0 10054 0
vsize: 40380
[startup+110.004 s]
Raw data (loadavg): 1.04 1.02 0.93 2/55 3122
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9397 0 0 0 10954 45 0 0 25 0 1 0 357746392 41349120 8819 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10095 8819 603 41 0 10054 0
vsize: 40380
[startup+120.004 s]
Raw data (loadavg): 1.04 1.02 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9430 0 0 0 11954 46 0 0 25 0 1 0 357746392 41611264 8852 4294967295 134512640 134672761 3221224560 3221222992 134604097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8852 603 41 0 10118 0
vsize: 40636
[startup+130.004 s]
Raw data (loadavg): 1.03 1.02 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9430 0 0 0 12954 46 0 0 25 0 1 0 357746392 41611264 8852 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8852 603 41 0 10118 0
vsize: 40636
[startup+140.005 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9435 0 0 0 13954 46 0 0 25 0 1 0 357746392 41611264 8857 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8857 603 41 0 10118 0
vsize: 40636
[startup+150.005 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9437 0 0 0 14954 46 0 0 25 0 1 0 357746392 41611264 8859 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8859 603 41 0 10118 0
vsize: 40636
[startup+160.006 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9439 0 0 0 15954 46 0 0 25 0 1 0 357746392 41611264 8861 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8861 603 41 0 10118 0
vsize: 40636
[startup+170.005 s]
Raw data (loadavg): 1.01 1.02 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9441 0 0 0 16954 46 0 0 25 0 1 0 357746392 41611264 8863 4294967295 134512640 134672761 3221224560 3221222984 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8863 603 41 0 10118 0
vsize: 40636
[startup+180.006 s]
Raw data (loadavg): 1.01 1.02 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9443 0 0 0 17954 46 0 0 25 0 1 0 357746392 41611264 8865 4294967295 134512640 134672761 3221224560 3221223072 134606994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8865 603 41 0 10118 0
vsize: 40636
[startup+190.006 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9446 0 0 0 18954 46 0 0 25 0 1 0 357746392 41611264 8868 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8868 603 41 0 10118 0
vsize: 40636
[startup+200.005 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9449 0 0 0 19954 47 0 0 25 0 1 0 357746392 41611264 8871 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8871 603 41 0 10118 0
vsize: 40636
[startup+210.006 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9452 0 0 0 20954 47 0 0 25 0 1 0 357746392 41611264 8874 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8874 603 41 0 10118 0
vsize: 40636
[startup+220.007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9455 0 0 0 21954 47 0 0 25 0 1 0 357746392 41611264 8877 4294967295 134512640 134672761 3221224560 3221223152 134607861 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10159 8877 603 41 0 10118 0
vsize: 40636
[startup+230.007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9479 0 0 0 22954 47 0 0 25 0 1 0 357746392 41619456 8855 4294967295 134512640 134672761 3221224560 3221223008 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10161 8855 603 41 0 10120 0
vsize: 40644
[startup+240.007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9479 0 0 0 23954 47 0 0 25 0 1 0 357746392 41619456 8855 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10161 8855 603 41 0 10120 0
vsize: 40644
[startup+250.007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 24953 48 0 0 25 0 1 0 357746392 42532864 9106 4294967295 134512640 134672761 3221224560 3221223024 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10384 9106 603 41 0 10343 0
vsize: 41536
[startup+260.007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 25953 48 0 0 25 0 1 0 357746392 42532864 9106 4294967295 134512640 134672761 3221224560 3221223056 134606420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10384 9106 603 41 0 10343 0
vsize: 41536
[startup+270.007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 26953 49 0 0 25 0 1 0 357746392 42532864 9106 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10384 9106 603 41 0 10343 0
vsize: 41536
[startup+280.008 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 27953 49 0 0 25 0 1 0 357746392 41226240 8814 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10065 8814 603 41 0 10024 0
vsize: 40260
[startup+290.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 28953 49 0 0 25 0 1 0 357746392 41226240 8814 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10065 8814 603 41 0 10024 0
vsize: 40260
[startup+300.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 10076 0 0 0 29952 50 0 0 25 0 1 0 357746392 42536960 9114 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9114 603 41 0 10344 0
vsize: 41540
[startup+310.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 30932 70 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134643719 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10311 603 41 0 11430 0
vsize: 45884
[startup+320.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 31838 138 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221222840 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10311 603 41 0 11430 0
vsize: 45884
[startup+330.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 32838 139 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10311 603 41 0 11430 0
vsize: 45884
[startup+340.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 33838 139 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10311 603 41 0 11430 0
vsize: 45884
[startup+350.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 34838 139 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10311 603 41 0 11430 0
vsize: 45884
[startup+360.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13298 0 0 0 35837 140 0 0 25 0 1 0 357746392 49004544 10603 4294967295 134512640 134672761 3221224560 3221222252 134566513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11964 10603 603 41 0 11923 0
vsize: 47856
[startup+370.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13298 0 0 0 36837 140 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10311 603 41 0 11430 0
vsize: 45884
[startup+380.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13298 0 0 0 37837 140 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10311 603 41 0 11430 0
vsize: 45884
[startup+390.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13620 0 0 0 38836 141 0 0 25 0 1 0 357746392 48365568 10633 4294967295 134512640 134672761 3221224560 3221223600 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11808 10633 603 41 0 11767 0
vsize: 47232
[startup+400.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 14430 0 0 0 39833 144 0 0 25 0 1 0 357746392 51757056 11443 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12636 11443 603 41 0 12595 0
vsize: 50544
[startup+410.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 15420 0 0 0 40831 147 0 0 25 0 1 0 357746392 55787520 12433 4294967295 134512640 134672761 3221224560 3221223760 134610694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13620 12433 603 41 0 13579 0
vsize: 54480
[startup+420.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 16402 0 0 0 41829 149 0 0 25 0 1 0 357746392 59817984 13415 4294967295 134512640 134672761 3221224560 3221223472 134644251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14604 13415 603 41 0 14563 0
vsize: 58416
[startup+430.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 16965 0 0 0 42828 150 0 0 25 0 1 0 357746392 62132224 13978 4294967295 134512640 134672761 3221224560 3221223696 134614513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15169 13978 603 41 0 15128 0
vsize: 60676
[startup+440.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 17625 0 0 0 43826 151 0 0 25 0 1 0 357746392 64864256 14638 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15836 14638 603 41 0 15795 0
vsize: 63344
[startup+450.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 18449 0 0 0 44824 153 0 0 25 0 1 0 357746392 68161536 15462 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16641 15462 603 41 0 16600 0
vsize: 66564
[startup+460.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 18876 0 0 0 45824 154 0 0 25 0 1 0 357746392 69873664 15889 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17059 15889 603 41 0 17018 0
vsize: 68236
[startup+470.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 21803 0 0 0 46802 176 0 0 25 0 1 0 357746392 75255808 17080 4294967295 134512640 134672761 3221224560 3221223104 134621095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18373 17080 603 41 0 18332 0
vsize: 73492
[startup+480.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 21815 0 0 0 47790 188 0 0 25 0 1 0 357746392 73490432 16789 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17942 16789 603 41 0 17901 0
vsize: 71768
[startup+490.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 21815 0 0 0 48790 188 0 0 25 0 1 0 357746392 73490432 16789 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17942 16789 603 41 0 17901 0
vsize: 71768
[startup+500.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24084 0 0 0 49766 213 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223232 134631080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 17095 603 41 0 19318 0
vsize: 77436
[startup+510.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24117 0 0 0 50677 275 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19359 17095 603 41 0 19318 0
vsize: 77436
[startup+520.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24117 0 0 0 51678 275 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 17095 603 41 0 19318 0
vsize: 77436
[startup+530.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24117 0 0 0 52678 275 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 17095 603 41 0 19318 0
vsize: 77436
[startup+540.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24408 0 0 0 53677 276 0 0 25 0 1 0 357746392 81244160 17386 4294967295 134512640 134672761 3221224560 3221223024 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19835 17386 603 41 0 19794 0
vsize: 79340
[startup+550.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24408 0 0 0 54677 276 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 17095 603 41 0 19318 0
vsize: 77436
[startup+560.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24408 0 0 0 55677 276 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 17095 603 41 0 19318 0
vsize: 77436
[startup+570.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24408 0 0 0 56677 277 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223648 1074743855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 17095 603 41 0 19318 0
vsize: 77436
[startup+580.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24410 0 0 0 57677 277 0 0 25 0 1 0 357746392 79294464 17097 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 17097 603 41 0 19318 0
vsize: 77436
[startup+590.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24412 0 0 0 58677 277 0 0 25 0 1 0 357746392 79294464 17099 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 17099 603 41 0 19318 0
vsize: 77436
[startup+600.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26820 0 0 0 59643 311 0 0 25 0 1 0 357746392 81489920 17437 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19895 17437 603 41 0 19854 0
vsize: 79580
[startup+610.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26820 0 0 0 60643 311 0 0 25 0 1 0 357746392 79466496 17145 4294967295 134512640 134672761 3221224560 3221223008 134643987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19401 17145 603 41 0 19360 0
vsize: 77604
[startup+620.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26821 0 0 0 61643 311 0 0 25 0 1 0 357746392 79466496 17146 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19401 17146 603 41 0 19360 0
vsize: 77604
[startup+630.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26822 0 0 0 62643 311 0 0 25 0 1 0 357746392 79466496 17147 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19401 17147 603 41 0 19360 0
vsize: 77604
[startup+640.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26991 0 0 0 63642 312 0 0 25 0 1 0 357746392 80388096 17316 4294967295 134512640 134672761 3221224560 3221223504 134606869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19626 17316 603 41 0 19585 0
vsize: 78504
[startup+650.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 27518 0 0 0 64641 313 0 0 25 0 1 0 357746392 82501632 17843 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20142 17843 603 41 0 20101 0
vsize: 80568
[startup+660.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 28356 0 0 0 65641 314 0 0 25 0 1 0 357746392 85876736 18681 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20966 18681 603 41 0 20925 0
vsize: 83864
[startup+670.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 28888 0 0 0 66639 315 0 0 25 0 1 0 357746392 88088576 19213 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19213 603 41 0 21465 0
vsize: 86024
[startup+680.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 29639 0 0 0 67638 317 0 0 25 0 1 0 357746392 91160576 19964 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22256 19964 603 41 0 22215 0
vsize: 89024
[startup+690.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 30510 0 0 0 68636 319 0 0 25 0 1 0 357746392 94679040 20835 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23115 20835 603 41 0 23074 0
vsize: 92460
[startup+700.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 31133 0 0 0 69635 320 0 0 25 0 1 0 357746392 97280000 21458 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23750 21458 603 41 0 23709 0
vsize: 95000
[startup+710.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 31804 0 0 0 70634 321 0 0 25 0 1 0 357746392 99966976 22129 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24406 22129 603 41 0 24365 0
vsize: 97624
[startup+720.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 32384 0 0 0 71632 323 0 0 25 0 1 0 357746392 102412288 22709 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25003 22709 603 41 0 24962 0
vsize: 100012
[startup+730.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 32766 0 0 0 72630 325 0 0 25 0 1 0 357746392 103968768 23091 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25383 23091 603 41 0 25342 0
vsize: 101532
[startup+740.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 33393 0 0 0 73630 326 0 0 25 0 1 0 357746392 106455040 23718 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25990 23718 603 41 0 25949 0
vsize: 103960
[startup+750.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 33834 0 0 0 74629 327 0 0 25 0 1 0 357746392 108355584 24159 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26454 24159 603 41 0 26413 0
vsize: 105816
[startup+760.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 34194 0 0 0 75628 328 0 0 25 0 1 0 357746392 109801472 24519 4294967295 134512640 134672761 3221224560 3221223704 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26807 24519 603 41 0 26766 0
vsize: 107228
[startup+770.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 34549 0 0 0 76628 328 0 0 25 0 1 0 357746392 111235072 24874 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27157 24874 603 41 0 27116 0
vsize: 108628
[startup+780.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 35204 0 0 0 77627 330 0 0 25 0 1 0 357746392 113946624 25529 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27819 25529 603 41 0 27778 0
vsize: 111276
[startup+790.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 35699 0 0 0 78626 330 0 0 25 0 1 0 357746392 115871744 26024 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28289 26024 603 41 0 28248 0
vsize: 113156
[startup+800.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 36177 0 0 0 79626 331 0 0 25 0 1 0 357746392 117911552 26502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28787 26502 603 41 0 28746 0
vsize: 115148
[startup+810.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 36734 0 0 0 80625 332 0 0 25 0 1 0 357746392 120123392 27059 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29327 27059 603 41 0 29286 0
vsize: 117308
[startup+820.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 37346 0 0 0 81624 334 0 0 25 0 1 0 357746392 122654720 27671 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29945 27671 603 41 0 29904 0
vsize: 119780
[startup+830.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 37876 0 0 0 82623 335 0 0 25 0 1 0 357746392 124751872 28201 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30457 28201 603 41 0 30416 0
vsize: 121828
[startup+840.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 38305 0 0 0 83622 336 0 0 25 0 1 0 357746392 126590976 28630 4294967295 134512640 134672761 3221224560 3221223716 134614480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30906 28630 603 41 0 30865 0
vsize: 123624
[startup+850.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 38989 0 0 0 84620 337 0 0 25 0 1 0 357746392 129331200 29314 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31575 29314 603 41 0 31534 0
vsize: 126300
[startup+860.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 39409 0 0 0 85619 338 0 0 25 0 1 0 357746392 131284992 29734 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32052 29734 603 41 0 32011 0
vsize: 128208
[startup+870.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 39777 0 0 0 86619 339 0 0 25 0 1 0 357746392 132820992 30102 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32427 30102 603 41 0 32386 0
vsize: 129708
[startup+880.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 40530 0 0 0 87617 341 0 0 25 0 1 0 357746392 135901184 30855 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33179 30855 603 41 0 33138 0
vsize: 132716
[startup+890.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 41036 0 0 0 88616 342 0 0 25 0 1 0 357746392 137990144 31361 4294967295 134512640 134672761 3221224560 3221223712 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33689 31361 603 41 0 33648 0
vsize: 134756
[startup+900.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 41672 0 0 0 89614 344 0 0 25 0 1 0 357746392 140591104 31997 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34324 31997 603 41 0 34283 0
vsize: 137296
[startup+910.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 41994 0 0 0 90614 345 0 0 25 0 1 0 357746392 141905920 32319 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34645 32319 603 41 0 34604 0
vsize: 138580
[startup+920.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 42661 0 0 0 91613 346 0 0 25 0 1 0 357746392 144642048 32986 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35313 32986 603 41 0 35272 0
vsize: 141252
[startup+930.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 43326 0 0 0 92611 348 0 0 25 0 1 0 357746392 147341312 33651 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35972 33651 603 41 0 35931 0
vsize: 143888
[startup+940.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 43934 0 0 0 93610 349 0 0 25 0 1 0 357746392 149803008 34259 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36573 34259 603 41 0 36532 0
vsize: 146292
[startup+950.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 44339 0 0 0 94610 350 0 0 25 0 1 0 357746392 151486464 34664 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36984 34664 603 41 0 36943 0
vsize: 147936
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 44750 0 0 0 95609 350 0 0 25 0 1 0 357746392 153165824 35075 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37394 35075 603 41 0 37353 0
vsize: 149576
[startup+970.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 45429 0 0 0 96608 352 0 0 25 0 1 0 357746392 155906048 35754 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38063 35754 603 41 0 38022 0
vsize: 152252
[startup+980.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 45770 0 0 0 97607 352 0 0 25 0 1 0 357746392 157339648 36095 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38413 36095 603 41 0 38372 0
vsize: 153652
[startup+990.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 46269 0 0 0 98606 354 0 0 25 0 1 0 357746392 159313920 36594 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38895 36594 603 41 0 38854 0
vsize: 155580
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 46487 0 0 0 99605 355 0 0 25 0 1 0 357746392 160206848 36812 4294967295 134512640 134672761 3221224560 3221223744 134615788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39113 36812 603 41 0 39072 0
vsize: 156452
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 47127 0 0 0 100603 357 0 0 25 0 1 0 357746392 162824192 37452 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39752 37452 603 41 0 39711 0
vsize: 159008
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 47787 0 0 0 101602 359 0 0 25 0 1 0 357746392 165617664 38112 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40434 38112 603 41 0 40393 0
vsize: 161736
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 48125 0 0 0 102601 360 0 0 25 0 1 0 357746392 166899712 38450 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40747 38450 603 41 0 40706 0
vsize: 162988
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 48561 0 0 0 103600 361 0 0 25 0 1 0 357746392 168693760 38886 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41185 38886 603 41 0 41144 0
vsize: 164740
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 48730 0 0 0 104599 361 0 0 25 0 1 0 357746392 169472000 39055 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41375 39055 603 41 0 41334 0
vsize: 165500
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 49025 0 0 0 105599 362 0 0 25 0 1 0 357746392 170618880 39350 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41655 39350 603 41 0 41614 0
vsize: 166620
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 49388 0 0 0 106598 363 0 0 25 0 1 0 357746392 172171264 39713 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42034 39713 603 41 0 41993 0
vsize: 168136
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 49882 0 0 0 107597 364 0 0 25 0 1 0 357746392 174125056 40207 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42511 40207 603 41 0 42470 0
vsize: 170044
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 50329 0 0 0 108596 365 0 0 25 0 1 0 357746392 175947776 40654 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42956 40654 603 41 0 42915 0
vsize: 171824
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 50673 0 0 0 109596 366 0 0 25 0 1 0 357746392 177307648 40998 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43288 40998 603 41 0 43247 0
vsize: 173152
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 51012 0 0 0 110595 367 0 0 25 0 1 0 357746392 178745344 41337 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43639 41337 603 41 0 43598 0
vsize: 174556
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 51353 0 0 0 111595 367 0 0 25 0 1 0 357746392 180183040 41678 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43990 41678 603 41 0 43949 0
vsize: 175960
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 51589 0 0 0 112594 368 0 0 25 0 1 0 357746392 181100544 41914 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44214 41914 603 41 0 44173 0
vsize: 176856
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 51909 0 0 0 113594 369 0 0 25 0 1 0 357746392 182386688 42234 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44528 42234 603 41 0 44487 0
vsize: 178112
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 52248 0 0 0 114593 369 0 0 25 0 1 0 357746392 183808000 42573 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44875 42573 603 41 0 44834 0
vsize: 179500
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 52568 0 0 0 115593 370 0 0 25 0 1 0 357746392 185126912 42893 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45197 42893 603 41 0 45156 0
vsize: 180788
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 52881 0 0 0 116592 371 0 0 25 0 1 0 357746392 186417152 43206 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45512 43206 603 41 0 45471 0
vsize: 182048
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 53356 0 0 0 117591 372 0 0 25 0 1 0 357746392 188358656 43681 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45986 43681 603 41 0 45945 0
vsize: 183944
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 53956 0 0 0 118590 373 0 0 25 0 1 0 357746392 190803968 44281 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46583 44281 603 41 0 46542 0
vsize: 186332
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 54293 0 0 0 119589 374 0 0 25 0 1 0 357746392 192212992 44618 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46927 44618 603 41 0 46886 0
vsize: 187708
[startup+1210.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 3124
Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 54585 0 0 0 120589 374 0 0 25 0 1 0 357746392 193376256 44910 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47211 44910 603 41 0 47170 0
vsize: 188844
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.18 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 3124
Raw data (stat): 3122 (minisat+) Z 3121 30927 30926 0 -1 12 54586 0 0 0 120589 391 0 0 25 0 1 0 357746392 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.18
CPU time (s): 1209.81
CPU user time (s): 1205.9
CPU system time (s): 3.91341
CPU usage (%): 99.9696
Max. virtual memory (Kb): 188844
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####