PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb53-24-opb/normalized-frb53-24-4.opb
MD5SUM	b7f280d80b52f97899362fbc10d59421
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-40
Optimality of the best value was proved	NO
Number of terms in the objective function	1272
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	1272
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	1272
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.12
Number of variables	1272
Total number of constraints	94308
Number of constraints which are clauses	94308
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5636

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        833148 kB
Buffers:         34932 kB
Cached:         125860 kB
SwapCached:       2476 kB
Active:          57348 kB
Inactive:       108796 kB
HighTotal:      131008 kB
HighFree:         2044 kB
LowTotal:       903652 kB
LowFree:        831104 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29792 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:27:33 (client local time) WITH STATUS 10 IN 1209.45 SECONDS
stats: 4102 7 1209.45 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94308 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 |   94308   188616 |   28292       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   94308   188616 |   37723       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 5.12522 s)
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70300     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  169359   364682 |   50807       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/51091          
c   -- var.elim.:  2000/51091          
c   -- var.elim.:  3000/51091          
c   -- var.elim.:  4000/51091          
c   -- var.elim.:  5000/51091          
c   -- var.elim.:  6000/51091          
c   -- var.elim.:  7000/51091          
c   -- var.elim.:  8000/51091          
c   -- var.elim.:  9000/51091          
c   -- var.elim.:  10000/51091          
c   -- var.elim.:  11000/51091          
c   -- var.elim.:  12000/51091          
c   -- var.elim.:  13000/51091          
c   -- var.elim.:  14000/51091          
c   -- var.elim.:  15000/51091          
c   -- var.elim.:  16000/51091          
c   -- var.elim.:  17000/51091          
c   -- var.elim.:  18000/51091          
c   -- var.elim.:  19000/51091          
c   -- var.elim.:  20000/51091          
c   -- var.elim.:  21000/51091          
c   -- var.elim.:  22000/51091          
c   -- var.elim.:  23000/51091          
c   -- var.elim.:  24000/51091          
c   -- var.elim.:  25000/51091          
c   -- var.elim.:  26000/51091          
c   -- var.elim.:  27000/51091          
c   -- var.elim.:  28000/51091          
c   -- var.elim.:  29000/51091          
c   -- var.elim.:  30000/51091          
c   -- var.elim.:  31000/51091          
c   -- var.elim.:  32000/51091          
c   -- var.elim.:  33000/51091          
c   -- var.elim.:  34000/51091          
c   -- var.elim.:  35000/51091          
c   -- var.elim.:  36000/51091          
c   -- var.elim.:  37000/51091          
c   -- var.elim.:  38000/51091          
c   -- var.elim.:  39000/51091          
c   -- var.elim.:  40000/51091          
c   -- var.elim.:  41000/51091          
c   -- var.elim.:  42000/51091          
c   -- var.elim.:  43000/51091          
c   -- var.elim.:  44000/51091          
c   -- var.elim.:  45000/51091          
c   -- var.elim.:  46000/51091          
c   -- var.elim.:  47000/51091          
c   -- var.elim.:  48000/51091          
c   -- var.elim.:  49000/51091          
c   -- var.elim.:  50000/51091          
c   -- var.elim.:  51000/51091          
c   -- var.elim.:  51091/51091          
c   -- var.elim.:  1000/25895          
c   -- var.elim.:  2000/25895          
c   -- var.elim.:  3000/25895          
c   -- var.elim.:  4000/25895          
c   -- var.elim.:  5000/25895          
c   -- var.elim.:  6000/25895          
c   -- var.elim.:  7000/25895          
c   -- var.elim.:  8000/25895          
c   -- var.elim.:  9000/25895          
c   -- var.elim.:  10000/25895          
c   -- var.elim.:  11000/25895          
c   -- var.elim.:  12000/25895          
c   -- var.elim.:  13000/25895          
c   -- var.elim.:  14000/25895          
c   -- var.elim.:  15000/25895          
c   -- var.elim.:  16000/25895          
c   -- var.elim.:  17000/25895          
c   -- var.elim.:  18000/25895          
c   -- var.elim.:  19000/25895          
c   -- var.elim.:  20000/25895          
c   -- var.elim.:  21000/25895          
c   -- var.elim.:  22000/25895          
c   -- var.elim.:  23000/25895          
c   -- var.elim.:  24000/25895          
c   -- var.elim.:  25000/25895          
c   -- var.elim.:  25895/25895          
c   -- var.elim.:  278/278          
c   -- var.elim.:  133/133          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  1000/9579          
c   -- var.elim.:  2000/9579          
c   -- var.elim.:  3000/9579          
c   -- var.elim.:  4000/9579          
c   -- var.elim.:  5000/9579          
c   -- var.elim.:  6000/9579          
c   -- var.elim.:  7000/9579          
c   -- var.elim.:  8000/9579          
c   -- var.elim.:  9000/9579          
c   -- var.elim.:  9579/9579          
c   -- var.elim.:  746/746          
c |         0 |  114671   370394 |      --       0       --      -- |     --   | -54688/5713
c |         0 |  114671   370394 |   45868       0        0     nan |  0.000 % |
c |       100 |  114665   370354 |   50452      99    20516   207.2 | 56.440 % |
c |       250 |  114665   370354 |   55497     249    38770   155.7 | 56.440 % |
c |       475 |  114665   370354 |   61047     474    78828   166.3 | 56.440 % |
c |       812 |  114665   370354 |   67152     811   134770   166.2 | 56.440 % |
c |      1319 |  114665   370354 |   73867    1318   225845   171.4 | 56.440 % |
c |      2078 |  114649   370161 |   81243    2074   402377   194.0 | 56.471 % |
c |      3218 |  114637   370017 |   89358    3211   624173   194.4 | 56.494 % |
c |      4926 |  114565   369328 |   98232    4912   998459   203.3 | 56.634 % |
c ==============================================================================
c (current CPU-time: 286.134 s)
c ==============================================================================
c [1mFound solution: -40[0m
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 |      6628 |  126279   400251 |   37883    6589  1406786   213.5 | 56.634 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21996          
c   -- var.elim.:  2000/21996          
c   -- var.elim.:  3000/21996          
c   -- var.elim.:  4000/21996          
c   -- var.elim.:  5000/21996          
c   -- var.elim.:  6000/21996          
c   -- var.elim.:  7000/21996          
c   -- var.elim.:  8000/21996          
c   -- var.elim.:  9000/21996          
c   -- var.elim.:  10000/21996          
c   -- var.elim.:  11000/21996          
c   -- var.elim.:  12000/21996          
c   -- var.elim.:  13000/21996          
c   -- var.elim.:  14000/21996          
c   -- var.elim.:  15000/21996          
c   -- var.elim.:  16000/21996          
c   -- var.elim.:  17000/21996          
c   -- var.elim.:  18000/21996          
c   -- var.elim.:  19000/21996          
c   -- var.elim.:  20000/21996          
c   -- var.elim.:  21000/21996          
c   -- var.elim.:  21996/21996          
c   -- var.elim.:  1000/8656          
c   -- var.elim.:  2000/8656          
c   -- var.elim.:  3000/8656          
c   -- var.elim.:  4000/8656          
c   -- var.elim.:  5000/8656          
c   -- var.elim.:  6000/8656          
c   -- var.elim.:  7000/8656          
c   -- var.elim.:  8000/8656          
c   -- var.elim.:  8656/8656          
c   -- var.elim.:  42/42          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c   -- var.elim.:  1000/7163          
c   -- var.elim.:  2000/7163          
c   -- var.elim.:  3000/7163          
c   -- var.elim.:  4000/7163          
c   -- var.elim.:  5000/7163          
c   -- var.elim.:  6000/7163          
c   -- var.elim.:  7000/7163          
c   -- var.elim.:  7163/7163          
c   -- var.elim.:  140/140          
c |      6628 |  114570   379139 |      --    6589       --      -- |     --   | -11685/-18903
c |      6628 |  114570   379139 |   45828    6460  1258156   194.8 | 56.634 % |
c |      6728 |  114492   378301 |   50376    6540  1265908   193.6 | 64.776 % |
c |      6878 |  114492   378301 |   55414    6690  1308699   195.6 | 64.776 % |
c |      7103 |  114492   378301 |   60955    6915  1355805   196.1 | 64.776 % |
c |      7440 |  114492   378301 |   67051    7252  1411182   194.6 | 64.776 % |
c |      7946 |  114322   376682 |   73646    7739  1537839   198.7 | 65.045 % |
c |      8705 |  114206   375561 |   80929    8477  1691864   199.6 | 65.229 % |
c |      9844 |  114114   374667 |   88950    9604  1942638   202.3 | 65.374 % |
c |     11555 |  113510   369041 |   97327   11285  2290458   203.0 | 66.330 % |
c |     14117 |  113252   366557 |  106816   13765  2880870   209.3 | 66.738 % |
c |     17961 |  113009   364170 |  117246   17550  3896602   222.0 | 67.118 % |
c |     23727 |  112550   359820 |  128447   23231  5461917   235.1 | 67.830 % |
c |     32376 |  111591   350485 |  140088   31691  7949814   250.9 | 69.311 % |
c ==============================================================================
c (current CPU-time: 546.221 s)
c ==============================================================================
c [1mFound solution: -41[0m
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 |     42735 |  113314   349073 |   33994   41826 11320665   270.7 | 69.311 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10688          
c   -- var.elim.:  2000/10688          
c   -- var.elim.:  3000/10688          
c   -- var.elim.:  4000/10688          
c   -- var.elim.:  5000/10688          
c   -- var.elim.:  6000/10688          
c   -- var.elim.:  7000/10688          
c   -- var.elim.:  8000/10688          
c   -- var.elim.:  9000/10688          
c   -- var.elim.:  10000/10688          
c   -- var.elim.:  10688/10688          
c   -- var.elim.:  1000/1822          
c   -- var.elim.:  1822/1822          
c |     42735 |  110772   343929 |      --   41826       --      -- |     --   | -2541/-5141
c |     42735 |  110772   343929 |   44308   41737 11303325   270.8 | 69.311 % |
c |     42835 |  110765   343849 |   48736   41835 11310664   270.4 | 71.027 % |
c |     42985 |  110723   343429 |   53589   41984 11342386   270.2 | 71.092 % |
c |     43210 |  110723   343429 |   58948   42209 11402474   270.1 | 71.092 % |
c |     43547 |  110693   343116 |   64826   42520 11478814   270.0 | 71.139 % |
c |     44053 |  110693   343116 |   71308   43026 11651584   270.8 | 71.139 % |
c |     44812 |  110593   342113 |   78368   43771 11904886   272.0 | 71.295 % |
c |     45951 |  110479   340910 |   86116   44882 12240242   272.7 | 71.467 % |
c |     47659 |  110437   340507 |   94692   46552 12791617   274.8 | 71.529 % |
c |     50221 |  110399   340140 |  104126   49107 13657714   278.1 | 71.589 % |
c |     54065 |  110214   338243 |  114346   52925 14743624   278.6 | 71.870 % |
c |     59831 |  109506   331312 |  124973   58506 16641969   284.4 | 72.953 % |
c |     68480 |  108898   325457 |  136707   66875 19389263   289.9 | 73.887 % |
c ==============================================================================
c (current CPU-time: 788.886 s)
c ==============================================================================
c [1mFound solution: -42[0m
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 |     71856 |  108845   324236 |   32653   70191 20470658   291.6 | 73.887 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7221          
c   -- var.elim.:  2000/7221          
c   -- var.elim.:  3000/7221          
c   -- var.elim.:  4000/7221          
c   -- var.elim.:  5000/7221          
c   -- var.elim.:  6000/7221          
c   -- var.elim.:  7000/7221          
c   -- var.elim.:  7221/7221          
c   -- var.elim.:  394/394          
c   -- subsuming                       
c   -- var.elim.:  160/160          
c |     71856 |  108727   322043 |      --   70191       --      -- |     --   | -101/-181
c |     71856 |  108727   322043 |   43490   70191 20470658   291.6 | 73.887 % |
c |     71956 |  108512   320142 |   47745   22026  2756653   125.2 | 74.545 % |
c |     72107 |  108512   320142 |   52519   22177  2783496   125.5 | 74.545 % |
c |     72333 |  108512   320142 |   57771   22403  2853148   127.4 | 74.545 % |
c |     72670 |  108504   320075 |   63544   22726  2954019   130.0 | 74.557 % |
c |     73176 |  108502   320052 |   69897   23229  3069045   132.1 | 74.560 % |
c |     73935 |  108502   320052 |   76887   23988  3288149   137.1 | 74.560 % |
c |     75074 |  108438   319418 |   84525   25118  3576009   142.4 | 74.660 % |
c |     76783 |  108290   317940 |   92851   26806  4013851   149.7 | 74.879 % |
c |     79345 |  108212   317184 |  102063   29363  4894579   166.7 | 74.995 % |
c |     83189 |  108080   315868 |  112132   33173  6050429   182.4 | 75.191 % |
c |     88955 |  107736   312338 |  122953   38864  7852343   202.0 | 75.700 % |
c |     97604 |  107374   308631 |  134794   47426 10992478   231.8 | 76.247 % |
c ==============================================================================
c (current CPU-time: 956.293 s)
c ==============================================================================
c [1mFound solution: -44[0m
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 |    101772 |  111901   319329 |   33570   51564 12552161   243.4 | 76.247 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10957          
c   -- var.elim.:  2000/10957          
c   -- var.elim.:  3000/10957          
c   -- var.elim.:  4000/10957          
c   -- var.elim.:  5000/10957          
c   -- var.elim.:  6000/10957          
c   -- var.elim.:  7000/10957          
c   -- var.elim.:  8000/10957          
c   -- var.elim.:  9000/10957          
c   -- var.elim.:  10000/10957          
c   -- var.elim.:  10957/10957          
c   -- var.elim.:  1000/3152          
c   -- var.elim.:  2000/3152          
c   -- var.elim.:  3000/3152          
c   -- var.elim.:  3152/3152          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/2958          
c   -- var.elim.:  2000/2958          
c   -- var.elim.:  2958/2958          
c   -- var.elim.:  234/234          
c   -- subsuming                       
c |    101772 |  107277   309355 |      --   51564       --      -- |     --   | -4579/-9587
c |    101772 |  107277   309355 |   42910   45639  7410512   162.4 | 76.247 % |
c |    101872 |  107245   308988 |   47187   45738  7419096   162.2 | 77.361 % |
c |    102022 |  107197   308537 |   51883   45887  7464876   162.7 | 77.431 % |
c |    102247 |  107197   308537 |   57071   46112  7492876   162.5 | 77.431 % |
c |    102584 |  107197   308537 |   62778   46449  7579269   163.2 | 77.431 % |
c |    103090 |  107197   308537 |   69056   46955  7727432   164.6 | 77.431 % |
c |    103849 |  107161   308215 |   75936   47701  7949496   166.7 | 77.485 % |
c |    104988 |  107055   307086 |   83447   48809  8225995   168.5 | 77.636 % |
c |    106697 |  107019   306695 |   91761   50493  8838790   175.0 | 77.691 % |
c |    109259 |  107019   306695 |  100938   53055  9664344   182.2 | 77.691 % |
c |    113103 |  106860   305137 |  110866   56876 10846476   190.7 | 77.917 % |
c |    118869 |  106636   302822 |  121697   62558 12485450   199.6 | 78.247 % |
c |    127519 |  106052   296902 |  133134   71030 15040254   211.7 | 79.078 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -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 -C325 C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -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): 0.86 0.95 0.90 2/54 28838
Raw data (stat): 28838 (runsolver) R 28837 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480510456 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.88 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10102 0 0 0 957 41 0 0 25 0 1 0 480510456 43253760 9511 4294967295 134512640 134672761 3221224560 3221222736 1075352388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10560 9511 603 41 0 10519 0
vsize: 42240
[startup+20.001 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10456 0 0 0 1954 44 0 0 25 0 1 0 480510456 44654592 9865 4294967295 134512640 134672761 3221224560 3221222816 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10902 9865 603 41 0 10861 0
vsize: 43608
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10462 0 0 0 2954 44 0 0 25 0 1 0 480510456 44654592 9871 4294967295 134512640 134672761 3221224560 3221223056 134644260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10902 9871 603 41 0 10861 0
vsize: 43608
[startup+40.0016 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10463 0 0 0 3954 44 0 0 25 0 1 0 480510456 44654592 9872 4294967295 134512640 134672761 3221224560 3221222992 134605852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10902 9872 603 41 0 10861 0
vsize: 43608
[startup+50.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10464 0 0 0 4953 44 0 0 25 0 1 0 480510456 44654592 9873 4294967295 134512640 134672761 3221224560 3221223008 134643636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10902 9873 603 41 0 10861 0
vsize: 43608
[startup+60.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10465 0 0 0 5953 44 0 0 25 0 1 0 480510456 44654592 9874 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10902 9874 603 41 0 10861 0
vsize: 43608
[startup+70.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10466 0 0 0 6953 44 0 0 25 0 1 0 480510456 44654592 9875 4294967295 134512640 134672761 3221224560 3221222992 134604097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10902 9875 603 41 0 10861 0
vsize: 43608
[startup+80.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10500 0 0 0 7953 44 0 0 25 0 1 0 480510456 44916736 9909 4294967295 134512640 134672761 3221224560 3221223152 134608016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 9909 603 41 0 10925 0
vsize: 43864
[startup+90.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10501 0 0 0 8954 44 0 0 25 0 1 0 480510456 44916736 9910 4294967295 134512640 134672761 3221224560 3221222448 134566548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 9910 603 41 0 10925 0
vsize: 43864
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10502 0 0 0 9954 44 0 0 25 0 1 0 480510456 44916736 9911 4294967295 134512640 134672761 3221224560 3221222992 134604682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 9911 603 41 0 10925 0
vsize: 43864
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10503 0 0 0 10954 45 0 0 25 0 1 0 480510456 44916736 9912 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 9912 603 41 0 10925 0
vsize: 43864
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10506 0 0 0 11954 45 0 0 25 0 1 0 480510456 44916736 9915 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 9915 603 41 0 10925 0
vsize: 43864
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10507 0 0 0 12954 45 0 0 25 0 1 0 480510456 44916736 9916 4294967295 134512640 134672761 3221224560 3221222992 134604019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 9916 603 41 0 10925 0
vsize: 43864
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10509 0 0 0 13954 45 0 0 25 0 1 0 480510456 44916736 9918 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 9918 603 41 0 10925 0
vsize: 43864
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10510 0 0 0 14954 45 0 0 25 0 1 0 480510456 44916736 9919 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 9919 603 41 0 10925 0
vsize: 43864
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10528 0 0 0 15954 45 0 0 25 0 1 0 480510456 45146112 9937 4294967295 134512640 134672761 3221224560 3221223056 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 9937 603 41 0 10981 0
vsize: 44088
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10531 0 0 0 16955 45 0 0 25 0 1 0 480510456 45146112 9940 4294967295 134512640 134672761 3221224560 3221222992 134604040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 9940 603 41 0 10981 0
vsize: 44088
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10533 0 0 0 17954 45 0 0 25 0 1 0 480510456 45146112 9942 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 9942 603 41 0 10981 0
vsize: 44088
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10539 0 0 0 18955 45 0 0 25 0 1 0 480510456 45146112 9948 4294967295 134512640 134672761 3221224560 3221223152 134608088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 9948 603 41 0 10981 0
vsize: 44088
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10543 0 0 0 19954 45 0 0 25 0 1 0 480510456 45146112 9952 4294967295 134512640 134672761 3221224560 3221223008 134643969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 9952 603 41 0 10981 0
vsize: 44088
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10543 0 0 0 20954 46 0 0 25 0 1 0 480510456 45146112 9952 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 9952 603 41 0 10981 0
vsize: 44088
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10875 0 0 0 21953 46 0 0 25 0 1 0 480510456 47620096 10284 4294967295 134512640 134672761 3221224560 3221222320 134566449 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11626 10284 603 41 0 11585 0
vsize: 46504
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10875 0 0 0 22953 46 0 0 25 0 1 0 480510456 47620096 10284 4294967295 134512640 134672761 3221224560 3221223024 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11626 10284 603 41 0 11585 0
vsize: 46504
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10875 0 0 0 23953 47 0 0 25 0 1 0 480510456 47620096 10284 4294967295 134512640 134672761 3221224560 3221223056 134606420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11626 10284 603 41 0 11585 0
vsize: 46504
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10875 0 0 0 24954 47 0 0 25 0 1 0 480510456 47620096 10284 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11626 10284 603 41 0 11585 0
vsize: 46504
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10875 0 0 0 25954 47 0 0 25 0 1 0 480510456 45146112 9952 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 9952 603 41 0 10981 0
vsize: 44088
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 10885 0 0 0 26954 47 0 0 25 0 1 0 480510456 45146112 9962 4294967295 134512640 134672761 3221224560 3221223504 134606420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 9962 603 41 0 10981 0
vsize: 44088
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 11411 0 0 0 27952 48 0 0 25 0 1 0 480510456 47255552 10488 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11537 10488 603 41 0 11496 0
vsize: 46148
[startup+290 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14225 0 0 0 28941 59 0 0 25 0 1 0 480510456 58716160 11959 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14335 11959 603 41 0 14294 0
vsize: 57340
[startup+300 s]
Raw data (loadavg): 1.07 0.99 0.91 1/54 28838
Raw data (stat): 28838 (minisat+) D 28837 22612 22611 0 -1 0 14225 0 0 0 29875 97 0 0 25 0 1 0 480510456 56078336 11627 4294967295 134512640 134672761 3221224560 3221222768 1075730206 0 0 5 16386 3222661533 0 0 17 1 0 0
Raw data (statm): 13691 11627 603 41 0 13650 0
vsize: 54764
[startup+310.001 s]
Raw data (loadavg): 1.22 1.02 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14225 0 0 0 30787 135 0 0 25 0 1 0 480510456 56078336 11627 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13691 11627 603 41 0 13650 0
vsize: 54764
[startup+320.002 s]
Raw data (loadavg): 1.18 1.02 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14225 0 0 0 31786 135 0 0 25 0 1 0 480510456 56078336 11627 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13691 11627 603 41 0 13650 0
vsize: 54764
[startup+330.002 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14225 0 0 0 32787 135 0 0 25 0 1 0 480510456 56078336 11627 4294967295 134512640 134672761 3221224560 3221223008 134643577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13691 11627 603 41 0 13650 0
vsize: 54764
[startup+340.002 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14557 0 0 0 33785 137 0 0 25 0 1 0 480510456 58716160 11959 4294967295 134512640 134672761 3221224560 3221223272 134643381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14335 11959 603 41 0 14294 0
vsize: 57340
[startup+350.001 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14557 0 0 0 34785 137 0 0 25 0 1 0 480510456 58716160 11959 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14335 11959 603 41 0 14294 0
vsize: 57340
[startup+360.001 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14557 0 0 0 35785 137 0 0 25 0 1 0 480510456 56078336 11627 4294967295 134512640 134672761 3221224560 3221222864 134621744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13691 11627 603 41 0 13650 0
vsize: 54764
[startup+370.001 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14558 0 0 0 36785 137 0 0 25 0 1 0 480510456 56078336 11628 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13691 11628 603 41 0 13650 0
vsize: 54764
[startup+380.002 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 14899 0 0 0 37785 137 0 0 25 0 1 0 480510456 57520128 11969 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14043 11969 603 41 0 14002 0
vsize: 56172
[startup+390.002 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 15441 0 0 0 38784 138 0 0 25 0 1 0 480510456 59715584 12511 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14579 12513 603 41 0 14538 0
vsize: 58316
[startup+400.002 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 16013 0 0 0 39783 140 0 0 25 0 1 0 480510456 62103552 13083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15162 13083 603 41 0 15121 0
vsize: 60648
[startup+410.002 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 16588 0 0 0 40781 142 0 0 25 0 1 0 480510456 64495616 13658 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 13658 603 41 0 15705 0
vsize: 62984
[startup+420.002 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 17081 0 0 0 41780 143 0 0 25 0 1 0 480510456 66478080 14151 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 14151 603 41 0 16189 0
vsize: 64920
[startup+430.003 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 17711 0 0 0 42778 145 0 0 25 0 1 0 480510456 69029888 14781 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16853 14781 603 41 0 16812 0
vsize: 67412
[startup+440.003 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 18329 0 0 0 43777 146 0 0 25 0 1 0 480510456 71630848 15399 4294967295 134512640 134672761 3221224560 3221223408 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17488 15399 603 41 0 17447 0
vsize: 69952
[startup+450.002 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 18873 0 0 0 44776 148 0 0 25 0 1 0 480510456 73879552 15943 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18037 15943 603 41 0 17996 0
vsize: 72148
[startup+460.003 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 19439 0 0 0 45774 149 0 0 25 0 1 0 480510456 76197888 16509 4294967295 134512640 134672761 3221224560 3221223704 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18603 16509 603 41 0 18562 0
vsize: 74412
[startup+470.003 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 19900 0 0 0 46774 150 0 0 25 0 1 0 480510456 78045184 16970 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 16970 603 41 0 19013 0
vsize: 76216
[startup+480.003 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 20375 0 0 0 47773 151 0 0 25 0 1 0 480510456 79974400 17445 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19525 17445 603 41 0 19484 0
vsize: 78100
[startup+490.004 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 20934 0 0 0 48772 153 0 0 25 0 1 0 480510456 82276352 18004 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20087 18004 603 41 0 20046 0
vsize: 80348
[startup+500.004 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 21635 0 0 0 49771 154 0 0 25 0 1 0 480510456 85254144 18705 4294967295 134512640 134672761 3221224560 3221223504 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20814 18705 603 41 0 20773 0
vsize: 83256
[startup+510.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 22063 0 0 0 50770 155 0 0 25 0 1 0 480510456 86949888 19133 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21228 19133 603 41 0 21187 0
vsize: 84912
[startup+520.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 22617 0 0 0 51769 156 0 0 25 0 1 0 480510456 89313280 19687 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21805 19687 603 41 0 21764 0
vsize: 87220
[startup+530.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 23060 0 0 0 52768 157 0 0 25 0 1 0 480510456 91099136 20130 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22241 20130 603 41 0 22200 0
vsize: 88964
[startup+540.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 23613 0 0 0 53766 159 0 0 25 0 1 0 480510456 93278208 20683 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22773 20683 603 41 0 22732 0
vsize: 91092
[startup+550.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 26727 0 0 0 54743 182 0 0 25 0 1 0 480510456 97701888 21715 4294967295 134512640 134672761 3221224560 3221223104 134621095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23853 21715 603 41 0 23812 0
vsize: 95412
[startup+560.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 26727 0 0 0 55738 188 0 0 25 0 1 0 480510456 95866880 21383 4294967295 134512640 134672761 3221224560 3221223008 134606413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23405 21383 603 41 0 23364 0
vsize: 93620
[startup+570.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 26727 0 0 0 56732 192 0 0 25 0 1 0 480510456 95866880 21383 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23405 21383 603 41 0 23364 0
vsize: 93620
[startup+580.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 26773 0 0 0 57733 193 0 0 25 0 1 0 480510456 96137216 21429 4294967295 134512640 134672761 3221224560 3221223744 134615649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23471 21429 603 41 0 23430 0
vsize: 93884
[startup+590.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 27353 0 0 0 58731 195 0 0 25 0 1 0 480510456 98480128 22009 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24043 22009 603 41 0 24002 0
vsize: 96172
[startup+600.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 27812 0 0 0 59729 196 0 0 25 0 1 0 480510456 100347904 22468 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24499 22468 603 41 0 24458 0
vsize: 97996
[startup+610.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 28316 0 0 0 60728 198 0 0 25 0 1 0 480510456 102440960 22972 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25010 22972 603 41 0 24969 0
vsize: 100040
[startup+620.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 29029 0 0 0 61725 200 0 0 25 0 1 0 480510456 105390080 23685 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25730 23685 603 41 0 25689 0
vsize: 102920
[startup+630.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 29377 0 0 0 62724 201 0 0 25 0 1 0 480510456 106692608 24033 4294967295 134512640 134672761 3221224560 3221223696 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26048 24033 603 41 0 26007 0
vsize: 104192
[startup+640.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 29896 0 0 0 63723 202 0 0 25 0 1 0 480510456 108888064 24552 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26584 24552 603 41 0 26543 0
vsize: 106336
[startup+650.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 30347 0 0 0 64722 204 0 0 25 0 1 0 480510456 110747648 25003 4294967295 134512640 134672761 3221224560 3221223704 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27038 25003 603 41 0 26997 0
vsize: 108152
[startup+660.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 30771 0 0 0 65720 205 0 0 25 0 1 0 480510456 112459776 25427 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27456 25427 603 41 0 27415 0
vsize: 109824
[startup+670.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 31390 0 0 0 66719 207 0 0 25 0 1 0 480510456 114905088 26046 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28053 26046 603 41 0 28012 0
vsize: 112212
[startup+680.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 31786 0 0 0 67718 208 0 0 25 0 1 0 480510456 116629504 26442 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28474 26442 603 41 0 28433 0
vsize: 113896
[startup+690.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 32176 0 0 0 68716 210 0 0 25 0 1 0 480510456 118198272 26832 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28857 26832 603 41 0 28816 0
vsize: 115428
[startup+700.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 32607 0 0 0 69715 211 0 0 25 0 1 0 480510456 119918592 27263 4294967295 134512640 134672761 3221224560 3221223232 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29277 27263 603 41 0 29236 0
vsize: 117108
[startup+710.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 32864 0 0 0 70714 212 0 0 25 0 1 0 480510456 120963072 27520 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29532 27520 603 41 0 29491 0
vsize: 118128
[startup+720.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 33432 0 0 0 71713 213 0 0 25 0 1 0 480510456 123293696 28088 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30101 28088 603 41 0 30060 0
vsize: 120404
[startup+730.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 33860 0 0 0 72712 215 0 0 25 0 1 0 480510456 125091840 28516 4294967295 134512640 134672761 3221224560 3221223704 134616132 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30540 28516 603 41 0 30499 0
vsize: 122160
[startup+740.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 34112 0 0 0 73710 216 0 0 25 0 1 0 480510456 126124032 28768 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30792 28768 603 41 0 30751 0
vsize: 123168
[startup+750.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 34460 0 0 0 74709 218 0 0 25 0 1 0 480510456 127819776 29116 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31206 29116 603 41 0 31165 0
vsize: 124824
[startup+760.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 34791 0 0 0 75708 219 0 0 25 0 1 0 480510456 129114112 29447 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31522 29447 603 41 0 31481 0
vsize: 126088
[startup+770.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 35015 0 0 0 76707 220 0 0 25 0 1 0 480510456 130007040 29671 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31740 29671 603 41 0 31699 0
vsize: 126960
[startup+780.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 35398 0 0 0 77707 220 0 0 25 0 1 0 480510456 131571712 30054 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32122 30054 603 41 0 32081 0
vsize: 128488
[startup+790.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 35823 0 0 0 78705 222 0 0 25 0 1 0 480510456 133386240 30479 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32565 30479 603 41 0 32524 0
vsize: 130260
[startup+800.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 38840 0 0 0 79680 247 0 0 25 0 1 0 480510456 134402048 30757 4294967295 134512640 134672761 3221224560 3221223008 134643584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30757 603 41 0 32772 0
vsize: 131252
[startup+810.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39241 0 0 0 80679 248 0 0 25 0 1 0 480510456 134402048 30757 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30757 603 41 0 32772 0
vsize: 131252
[startup+820.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39241 0 0 0 81679 248 0 0 25 0 1 0 480510456 134402048 30757 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30757 603 41 0 32772 0
vsize: 131252
[startup+830.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39241 0 0 0 82679 249 0 0 25 0 1 0 480510456 134402048 30757 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30757 603 41 0 32772 0
vsize: 131252
[startup+840.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39241 0 0 0 83679 249 0 0 25 0 1 0 480510456 134402048 30757 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30757 603 41 0 32772 0
vsize: 131252
[startup+850.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39241 0 0 0 84679 249 0 0 25 0 1 0 480510456 134402048 30757 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30757 603 41 0 32772 0
vsize: 131252
[startup+860.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39241 0 0 0 85678 250 0 0 25 0 1 0 480510456 134402048 30757 4294967295 134512640 134672761 3221224560 3221223568 134522547 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30757 603 41 0 32772 0
vsize: 131252
[startup+870.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 86678 250 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+880.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 87678 250 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+890.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 88678 251 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221223704 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+900.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 89678 251 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+910.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 90678 251 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221223712 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+920.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 91678 251 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+930.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 92677 252 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+940.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 93677 252 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221222744 134566604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+950.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 39242 0 0 0 94677 252 0 0 25 0 1 0 480510456 134402048 30758 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 30758 603 41 0 32772 0
vsize: 131252
[startup+960.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 40981 0 0 0 95669 260 0 0 25 0 1 0 480510456 146919424 32403 4294967295 134512640 134672761 3221224560 3221223008 134565189 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35869 32403 603 41 0 35828 0
vsize: 143476
[startup+970.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 41545 0 0 0 96636 293 0 0 25 0 1 0 480510456 134303744 30850 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32789 30850 603 41 0 32748 0
vsize: 131156
[startup+980.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 41545 0 0 0 97635 294 0 0 25 0 1 0 480510456 134303744 30850 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32789 30850 603 41 0 32748 0
vsize: 131156
[startup+990.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42231 0 0 0 98633 296 0 0 25 0 1 0 480510456 134565888 30883 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32853 30883 603 41 0 32812 0
vsize: 131412
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42231 0 0 0 99632 296 0 0 25 0 1 0 480510456 134565888 30883 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32853 30883 603 41 0 32812 0
vsize: 131412
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42231 0 0 0 100632 297 0 0 25 0 1 0 480510456 134565888 30883 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30883 603 41 0 32812 0
vsize: 131412
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42231 0 0 0 101632 297 0 0 25 0 1 0 480510456 134565888 30883 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30883 603 41 0 32812 0
vsize: 131412
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42231 0 0 0 102632 297 0 0 25 0 1 0 480510456 134565888 30883 4294967295 134512640 134672761 3221224560 3221223744 134615722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30883 603 41 0 32812 0
vsize: 131412
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42231 0 0 0 103632 297 0 0 25 0 1 0 480510456 134565888 30883 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30883 603 41 0 32812 0
vsize: 131412
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 104632 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 105632 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223728 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 106632 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 107633 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223704 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 108633 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 109633 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 110633 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 111633 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 112633 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 113634 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42232 0 0 0 114634 297 0 0 25 0 1 0 480510456 134565888 30884 4294967295 134512640 134672761 3221224560 3221223504 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30884 603 41 0 32812 0
vsize: 131412
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42233 0 0 0 115634 297 0 0 25 0 1 0 480510456 134565888 30885 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30885 603 41 0 32812 0
vsize: 131412
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42234 0 0 0 116634 297 0 0 25 0 1 0 480510456 134565888 30886 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30886 603 41 0 32812 0
vsize: 131412
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42235 0 0 0 117634 297 0 0 25 0 1 0 480510456 134565888 30887 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30887 603 41 0 32812 0
vsize: 131412
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42237 0 0 0 118634 297 0 0 25 0 1 0 480510456 134565888 30889 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30889 603 41 0 32812 0
vsize: 131412
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42238 0 0 0 119634 297 0 0 25 0 1 0 480510456 134565888 30890 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30890 603 41 0 32812 0
vsize: 131412
[startup+1210.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28838 (minisat+) R 28837 22612 22611 0 -1 0 42240 0 0 0 120634 297 0 0 25 0 1 0 480510456 134565888 30892 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32853 30892 603 41 0 32812 0
vsize: 131412
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.14 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 28838
Raw data (stat): 28838 (minisat+) Z 28837 22612 22611 0 -1 12 42241 0 0 0 120635 309 0 0 25 0 1 0 480510456 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.14
CPU time (s): 1209.45
CPU user time (s): 1206.35
CPU system time (s): 3.09653
CPU usage (%): 99.9427
Max. virtual memory (Kb): 143476
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####