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/frb59-26-opb/normalized-frb59-26-1.opb
MD5SUM	42c2d619b73aa24781f1b54bddde28cc
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-44
Optimality of the best value was proved	NO
Number of terms in the objective function	1534
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	1534
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	1534
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.13
Number of variables	1534
Total number of constraints	126555
Number of constraints which are clauses	126555
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 5645

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890872 kB
Buffers:         35948 kB
Cached:          87180 kB
SwapCached:        564 kB
Active:          56076 kB
Inactive:        70544 kB
HighTotal:      131008 kB
HighFree:        39816 kB
LowTotal:       903652 kB
LowFree:        851056 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11524 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:30:42 (client local time) WITH STATUS 10 IN 1209.76 SECONDS
stats: 4109 7 1209.76 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 126555 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 |  126555   253110 |   37966       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |  126555   253110 |   50622       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 7.41487 s)
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:85954     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  217075   465456 |   65122       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/61620          
c   -- var.elim.:  2000/61620          
c   -- var.elim.:  3000/61620          
c   -- var.elim.:  4000/61620          
c   -- var.elim.:  5000/61620          
c   -- var.elim.:  6000/61620          
c   -- var.elim.:  7000/61620          
c   -- var.elim.:  8000/61620          
c   -- var.elim.:  9000/61620          
c   -- var.elim.:  10000/61620          
c   -- var.elim.:  11000/61620          
c   -- var.elim.:  12000/61620          
c   -- var.elim.:  13000/61620          
c   -- var.elim.:  14000/61620          
c   -- var.elim.:  15000/61620          
c   -- var.elim.:  16000/61620          
c   -- var.elim.:  17000/61620          
c   -- var.elim.:  18000/61620          
c   -- var.elim.:  19000/61620          
c   -- var.elim.:  20000/61620          
c   -- var.elim.:  21000/61620          
c   -- var.elim.:  22000/61620          
c   -- var.elim.:  23000/61620          
c   -- var.elim.:  24000/61620          
c   -- var.elim.:  25000/61620          
c   -- var.elim.:  26000/61620          
c   -- var.elim.:  27000/61620          
c   -- var.elim.:  28000/61620          
c   -- var.elim.:  29000/61620          
c   -- var.elim.:  30000/61620          
c   -- var.elim.:  31000/61620          
c   -- var.elim.:  32000/61620          
c   -- var.elim.:  33000/61620          
c   -- var.elim.:  34000/61620          
c   -- var.elim.:  35000/61620          
c   -- var.elim.:  36000/61620          
c   -- var.elim.:  37000/61620          
c   -- var.elim.:  38000/61620          
c   -- var.elim.:  39000/61620          
c   -- var.elim.:  40000/61620          
c   -- var.elim.:  41000/61620          
c   -- var.elim.:  42000/61620          
c   -- var.elim.:  43000/61620          
c   -- var.elim.:  44000/61620          
c   -- var.elim.:  45000/61620          
c   -- var.elim.:  46000/61620          
c   -- var.elim.:  47000/61620          
c   -- var.elim.:  48000/61620          
c   -- var.elim.:  49000/61620          
c   -- var.elim.:  50000/61620          
c   -- var.elim.:  51000/61620          
c   -- var.elim.:  52000/61620          
c   -- var.elim.:  53000/61620          
c   -- var.elim.:  54000/61620          
c   -- var.elim.:  55000/61620          
c   -- var.elim.:  56000/61620          
c   -- var.elim.:  57000/61620          
c   -- var.elim.:  58000/61620          
c   -- var.elim.:  59000/61620          
c   -- var.elim.:  60000/61620          
c   -- var.elim.:  61000/61620          
c   -- var.elim.:  61620/61620          
c   -- var.elim.:  1000/31158          
c   -- var.elim.:  2000/31158          
c   -- var.elim.:  3000/31158          
c   -- var.elim.:  4000/31158          
c   -- var.elim.:  5000/31158          
c   -- var.elim.:  6000/31158          
c   -- var.elim.:  7000/31158          
c   -- var.elim.:  8000/31158          
c   -- var.elim.:  9000/31158          
c   -- var.elim.:  10000/31158          
c   -- var.elim.:  11000/31158          
c   -- var.elim.:  12000/31158          
c   -- var.elim.:  13000/31158          
c   -- var.elim.:  14000/31158          
c   -- var.elim.:  15000/31158          
c   -- var.elim.:  16000/31158          
c   -- var.elim.:  17000/31158          
c   -- var.elim.:  18000/31158          
c   -- var.elim.:  19000/31158          
c   -- var.elim.:  20000/31158          
c   -- var.elim.:  21000/31158          
c   -- var.elim.:  22000/31158          
c   -- var.elim.:  23000/31158          
c   -- var.elim.:  24000/31158          
c   -- var.elim.:  25000/31158          
c   -- var.elim.:  26000/31158          
c   -- var.elim.:  27000/31158          
c   -- var.elim.:  28000/31158          
c   -- var.elim.:  29000/31158          
c   -- var.elim.:  30000/31158          
c   -- var.elim.:  31000/31158          
c   -- var.elim.:  31158/31158          
c   -- var.elim.:  1000/7275          
c   -- var.elim.:  2000/7275          
c   -- var.elim.:  3000/7275          
c   -- var.elim.:  4000/7275          
c   -- var.elim.:  5000/7275          
c   -- var.elim.:  6000/7275          
c   -- var.elim.:  7000/7275          
c   -- var.elim.:  7275/7275          
c   -- var.elim.:  94/94          
c   -- subsuming                       
c   -- var.elim.:  1000/11671          
c   -- var.elim.:  2000/11671          
c   -- var.elim.:  3000/11671          
c   -- var.elim.:  4000/11671          
c   -- var.elim.:  5000/11671          
c   -- var.elim.:  6000/11671          
c   -- var.elim.:  7000/11671          
c   -- var.elim.:  8000/11671          
c   -- var.elim.:  9000/11671          
c   -- var.elim.:  10000/11671          
c   -- var.elim.:  11000/11671          
c   -- var.elim.:  11671/11671          
c   -- var.elim.:  206/206          
c |         0 |  151128   474192 |      --       0       --      -- |     --   | -65941/8754
c |         0 |  151128   474192 |   60451       0        0     nan |  0.000 % |
c |       100 |  151128   474192 |   66496     100    15350   153.5 | 56.252 % |
c |       250 |  151128   474192 |   73145     250    45883   183.5 | 56.252 % |
c |       475 |  151128   474192 |   80460     475    96075   202.3 | 56.252 % |
c |       812 |  151112   474000 |   88497     808   154081   190.7 | 56.278 % |
c |      1319 |  151112   474000 |   97346    1315   248960   189.3 | 56.278 % |
c |      2079 |  151112   474000 |  107081    2075   419119   202.0 | 56.278 % |
c ==============================================================================
c (current CPU-time: 361.283 s)
c ==============================================================================
c [1mFound solution: -43[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 |      2497 |  166023   514475 |   49806    2493   515148   206.6 | 56.278 % |
c   -- subsuming                       
c   -- var.elim.:  1000/26157          
c   -- var.elim.:  2000/26157          
c   -- var.elim.:  3000/26157          
c   -- var.elim.:  4000/26157          
c   -- var.elim.:  5000/26157          
c   -- var.elim.:  6000/26157          
c   -- var.elim.:  7000/26157          
c   -- var.elim.:  8000/26157          
c   -- var.elim.:  9000/26157          
c   -- var.elim.:  10000/26157          
c   -- var.elim.:  11000/26157          
c   -- var.elim.:  12000/26157          
c   -- var.elim.:  13000/26157          
c   -- var.elim.:  14000/26157          
c   -- var.elim.:  15000/26157          
c   -- var.elim.:  16000/26157          
c   -- var.elim.:  17000/26157          
c   -- var.elim.:  18000/26157          
c   -- var.elim.:  19000/26157          
c   -- var.elim.:  20000/26157          
c   -- var.elim.:  21000/26157          
c   -- var.elim.:  22000/26157          
c   -- var.elim.:  23000/26157          
c   -- var.elim.:  24000/26157          
c   -- var.elim.:  25000/26157          
c   -- var.elim.:  26000/26157          
c   -- var.elim.:  26157/26157          
c   -- var.elim.:  1000/10723          
c   -- var.elim.:  2000/10723          
c   -- var.elim.:  3000/10723          
c   -- var.elim.:  4000/10723          
c   -- var.elim.:  5000/10723          
c   -- var.elim.:  6000/10723          
c   -- var.elim.:  7000/10723          
c   -- var.elim.:  8000/10723          
c   -- var.elim.:  9000/10723          
c   -- var.elim.:  10000/10723          
c   -- var.elim.:  10723/10723          
c   -- var.elim.:  52/52          
c   -- var.elim.:  116/116          
c   -- var.elim.:  27/27          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c   -- var.elim.:  1000/8959          
c   -- var.elim.:  2000/8959          
c   -- var.elim.:  3000/8959          
c   -- var.elim.:  4000/8959          
c   -- var.elim.:  5000/8959          
c   -- var.elim.:  6000/8959          
c   -- var.elim.:  7000/8959          
c   -- var.elim.:  8000/8959          
c   -- var.elim.:  8959/8959          
c   -- var.elim.:  146/146          
c |      2497 |  151436   492641 |      --    2493       --      -- |     --   | -14567/-21793
c |      2497 |  151436   492641 |   60574    2493   515148   206.6 | 56.278 % |
c |      2598 |  151436   492641 |   66631    2594   539328   207.9 | 64.009 % |
c |      2748 |  151436   492641 |   73295    2744   595560   217.0 | 64.009 % |
c |      2973 |  151436   492641 |   80624    2969   647402   218.1 | 64.009 % |
c |      3310 |  151436   492641 |   88686    3306   730403   220.9 | 64.009 % |
c |      3816 |  151436   492641 |   97555    3812   871047   228.5 | 64.009 % |
c |      4575 |  151408   492384 |  107291    4567  1036356   226.9 | 64.046 % |
c |      5715 |  151408   492384 |  118020    5707  1345389   235.7 | 64.046 % |
c |      7423 |  151308   491374 |  129736    7409  1783794   240.8 | 64.177 % |
c |      9985 |  151056   488935 |  142472    9938  2427776   244.3 | 64.509 % |
c |     13829 |  150938   487806 |  156597   13769  3544647   257.4 | 64.664 % |
c |     19595 |  150294   481640 |  171522   19453  5327470   273.9 | 65.511 % |
c |     28245 |  149228   471457 |  187336   27912  8085045   289.7 | 66.909 % |
c |     41219 |  148576   464946 |  205169   40724 12952793   318.1 | 67.751 % |
c ==============================================================================
c (current CPU-time: 802.509 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 |     54898 |  149864   461146 |   44959   54189 18601843   343.3 | 67.751 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13560          
c   -- var.elim.:  2000/13560          
c   -- var.elim.:  3000/13560          
c   -- var.elim.:  4000/13560          
c   -- var.elim.:  5000/13560          
c   -- var.elim.:  6000/13560          
c   -- var.elim.:  7000/13560          
c   -- var.elim.:  8000/13560          
c   -- var.elim.:  9000/13560          
c   -- var.elim.:  10000/13560          
c   -- var.elim.:  11000/13560          
c   -- var.elim.:  12000/13560          
c   -- var.elim.:  13000/13560          
c   -- var.elim.:  13560/13560          
c   -- var.elim.:  1000/1627          
c   -- var.elim.:  1627/1627          
c |     54898 |  147564   454267 |      --   54189       --      -- |     --   | -2281/-4955
c |     54898 |  147564   454267 |   59025   48475 10367485   213.9 | 67.751 % |
c |     54999 |  147564   454267 |   64928   48576 10400767   214.1 | 69.137 % |
c |     55149 |  147564   454267 |   71420   48726 10451502   214.5 | 69.137 % |
c |     55374 |  147564   454267 |   78563   48951 10528754   215.1 | 69.137 % |
c |     55711 |  147564   454267 |   86419   49288 10657908   216.2 | 69.137 % |
c |     56217 |  147564   454267 |   95061   49794 10836294   217.6 | 69.137 % |
c |     56976 |  147564   454267 |  104567   50553 11156006   220.7 | 69.137 % |
c |     58115 |  147564   454267 |  115024   51692 11550375   223.4 | 69.137 % |
c |     59823 |  147528   453915 |  126495   53393 12229366   229.0 | 69.184 % |
c |     62385 |  147429   452876 |  139051   55935 13401069   239.6 | 69.310 % |
c |     66229 |  147312   451664 |  152835   59712 15010195   251.4 | 69.460 % |
c |     71995 |  147234   450873 |  168030   65463 17924840   273.8 | 69.562 % |
c |     80645 |  146908   447484 |  184424   74017 22003347   297.3 | 69.985 % |
c ==============================================================================
c (current CPU-time: 1110.08 s)
c ==============================================================================
c [1mFound solution: -47[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 |     91000 |  157089   474581 |   47126   84340 27560750   326.8 | 69.985 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21110          
c   -- var.elim.:  2000/21110          
c   -- var.elim.:  3000/21110          
c   -- var.elim.:  4000/21110          
c   -- var.elim.:  5000/21110          
c   -- var.elim.:  6000/21110          
c   -- var.elim.:  7000/21110          
c   -- var.elim.:  8000/21110          
c   -- var.elim.:  9000/21110          
c   -- var.elim.:  10000/21110          
c   -- var.elim.:  11000/21110          
c   -- var.elim.:  12000/21110          
c   -- var.elim.:  13000/21110          
c   -- var.elim.:  14000/21110          
c   -- var.elim.:  15000/21110          
c   -- var.elim.:  16000/21110          
c   -- var.elim.:  17000/21110          
c   -- var.elim.:  18000/21110          
c   -- var.elim.:  19000/21110          
c   -- var.elim.:  20000/21110          
c   -- var.elim.:  21000/21110          
c   -- var.elim.:  21110/21110          
c   -- var.elim.:  1000/7583          
c   -- var.elim.:  2000/7583          
c   -- var.elim.:  3000/7583          
c   -- var.elim.:  4000/7583          
c   -- var.elim.:  5000/7583          
c   -- var.elim.:  6000/7583          
c   -- var.elim.:  7000/7583          
c   -- var.elim.:  7583/7583          
c   -- var.elim.:  51/51          
c   -- subsuming                       
c   -- var.elim.:  1000/6991          
c   -- var.elim.:  2000/6991          
c   -- var.elim.:  3000/6991          
c   -- var.elim.:  4000/6991          
c   -- var.elim.:  5000/6991          
c   -- var.elim.:  6000/6991          
c   -- var.elim.:  6991/6991          
c   -- var.elim.:  242/242          
c |     91000 |  147022   459815 |      --   84340       --      -- |     --   | -10034/-14699
c |     91000 |  147022   459815 |   58808   83747 27140003   324.1 | 69.985 % |
c |     91101 |  147022   459815 |   64689   83848 27162344   323.9 | 71.855 % |
c |     91251 |  147022   459815 |   71158   83998 27230958   324.2 | 71.855 % |
c |     91476 |  147022   459815 |   78274   84223 27286808   324.0 | 71.855 % |
c |     91813 |  146952   459152 |   86060   84557 27472965   324.9 | 71.933 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1534 -C1533 -C1532 -C1531 -C1530 -C1529 -C1528 -C1527 -C1526 -C1525 -C1524 -C1523 -C1522 -C1521 -C1520 -C1519 -C1518 -C1517 -C1516 -C1515 -C1514 -C1513 -C1512 -C1511 -C1510 -C1509 -C1508 -C1507 -C1506 -C1505 -C1504 -C1503 -C1502 -C1501 -C1500 -C1499 -C1498 -C1497 -C1496 -C1495 -C1494 -C1493 -C1492 -C1491 -C1490 -C1489 -C1488 -C1487 -C1486 -C1485 -C1484 -C1483 -C1482 -C1481 -C1480 -C1479 -C1478 -C1477 -C1476 -C1475 -C1474 -C1473 -C1472 -C1471 C1470 -C1469 -C1468 -C1467 -C1466 -C1465 -C1464 -C1463 -C1462 -C1461 -C1460 -C1459 -C1458 -C1457 C1456 -C1455 -C1454 -C1453 -C1452 -C1451 -C1450 -C1449 -C1448 -C1447 -C1446 -C1445 -C1444 -C1443 -C1442 -C1441 -C1440 -C1439 -C1438 -C1437 -C1436 -C1435 -C1434 -C1433 -C1432 -C1431 -C1430 -C1429 -C1428 -C1427 -C1426 -C1425 -C1424 -C1423 -C1422 -C1421 -C1420 -C1419 -C1418 -C1417 -C1416 -C1415 -C1414 -C1413 -C1412 -C1411 -C1410 -C1409 -C1408 -C1407 -C1406 -C1405 -C1404 -C1403 -C1402 C1401 -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 -C1386 -C1385 -C1384 -C1383 -C1382 -C1381 -C1380 -C1379 -C1378 C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 -C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 C1338 -C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 -C1327 C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 -C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 -C1273 -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 -C22#### 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.85 0.94 0.90 2/54 2598
Raw data (stat): 2598 (runsolver) R 2597 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422303328 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+9.99992 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 11971 0 0 0 960 37 0 0 25 0 1 0 422303328 48971776 11127 4294967295 134512640 134672761 3221224560 3221222880 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11956 11127 603 41 0 11915 0
vsize: 47824
[startup+19.9997 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12939 0 0 0 1937 60 0 0 25 0 1 0 422303328 52985856 12095 4294967295 134512640 134672761 3221224560 3221222288 134566482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12936 12095 603 41 0 12895 0
vsize: 51744
[startup+30.0005 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12945 0 0 0 2937 60 0 0 25 0 1 0 422303328 52985856 12101 4294967295 134512640 134672761 3221224560 3221222992 134604084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12936 12101 603 41 0 12895 0
vsize: 51744
[startup+40.0002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12945 0 0 0 3937 60 0 0 25 0 1 0 422303328 52985856 12101 4294967295 134512640 134672761 3221224560 3221222416 134566562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12936 12101 603 41 0 12895 0
vsize: 51744
[startup+50 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12978 0 0 0 4936 61 0 0 25 0 1 0 422303328 53248000 12134 4294967295 134512640 134672761 3221224560 3221223056 134644281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12134 603 41 0 12959 0
vsize: 52000
[startup+60.0001 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12980 0 0 0 5936 61 0 0 25 0 1 0 422303328 53248000 12136 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12136 603 41 0 12959 0
vsize: 52000
[startup+70.0005 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12981 0 0 0 6937 61 0 0 25 0 1 0 422303328 53248000 12137 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12137 603 41 0 12959 0
vsize: 52000
[startup+80.0013 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12982 0 0 0 7937 61 0 0 25 0 1 0 422303328 53248000 12138 4294967295 134512640 134672761 3221224560 3221222992 134604094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12138 603 41 0 12959 0
vsize: 52000
[startup+90.001 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12983 0 0 0 8937 61 0 0 25 0 1 0 422303328 53248000 12139 4294967295 134512640 134672761 3221224560 3221222784 1075350746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12139 603 41 0 12959 0
vsize: 52000
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12984 0 0 0 9937 61 0 0 25 0 1 0 422303328 53248000 12140 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12140 603 41 0 12959 0
vsize: 52000
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12985 0 0 0 10937 61 0 0 25 0 1 0 422303328 53248000 12141 4294967295 134512640 134672761 3221224560 3221223056 134644283 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12141 603 41 0 12959 0
vsize: 52000
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12986 0 0 0 11937 61 0 0 25 0 1 0 422303328 53248000 12142 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12142 603 41 0 12959 0
vsize: 52000
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12988 0 0 0 12938 61 0 0 25 0 1 0 422303328 53248000 12144 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12144 603 41 0 12959 0
vsize: 52000
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12989 0 0 0 13938 61 0 0 25 0 1 0 422303328 53248000 12145 4294967295 134512640 134672761 3221224560 3221222992 134605574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12145 603 41 0 12959 0
vsize: 52000
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12990 0 0 0 14938 61 0 0 25 0 1 0 422303328 53248000 12146 4294967295 134512640 134672761 3221224560 3221222816 134621268 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12146 603 41 0 12959 0
vsize: 52000
[startup+160.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 12992 0 0 0 15938 61 0 0 25 0 1 0 422303328 53248000 12148 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12148 603 41 0 12959 0
vsize: 52000
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13011 0 0 0 16938 61 0 0 25 0 1 0 422303328 53506048 12167 4294967295 134512640 134672761 3221224560 3221222992 134605450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13063 12167 603 41 0 13022 0
vsize: 52252
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13013 0 0 0 17938 61 0 0 25 0 1 0 422303328 53506048 12169 4294967295 134512640 134672761 3221224560 3221222764 134642887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13063 12169 603 41 0 13022 0
vsize: 52252
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13017 0 0 0 18939 61 0 0 25 0 1 0 422303328 53506048 12173 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13063 12173 603 41 0 13022 0
vsize: 52252
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13021 0 0 0 19939 61 0 0 25 0 1 0 422303328 53506048 12177 4294967295 134512640 134672761 3221224560 3221221856 134566712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13063 12177 603 41 0 13022 0
vsize: 52252
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13025 0 0 0 20939 61 0 0 25 0 1 0 422303328 53506048 12181 4294967295 134512640 134672761 3221224560 3221222992 134604069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13063 12181 603 41 0 13022 0
vsize: 52252
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13030 0 0 0 21939 61 0 0 25 0 1 0 422303328 53506048 12186 4294967295 134512640 134672761 3221224560 3221222928 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13063 12186 603 41 0 13022 0
vsize: 52252
[startup+230.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13034 0 0 0 22939 61 0 0 25 0 1 0 422303328 53506048 12190 4294967295 134512640 134672761 3221224560 3221223056 134644251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13063 12190 603 41 0 13022 0
vsize: 52252
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13039 0 0 0 23939 61 0 0 25 0 1 0 422303328 53506048 12195 4294967295 134512640 134672761 3221224560 3221223088 134606420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13063 12195 603 41 0 13022 0
vsize: 52252
[startup+250 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13043 0 0 0 24939 61 0 0 25 0 1 0 422303328 53768192 12199 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13127 12199 603 41 0 13086 0
vsize: 52508
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13075 0 0 0 25939 61 0 0 25 0 1 0 422303328 53518336 12170 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13066 12170 603 41 0 13025 0
vsize: 52264
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13075 0 0 0 26939 61 0 0 25 0 1 0 422303328 53518336 12170 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13066 12170 603 41 0 13025 0
vsize: 52264
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13075 0 0 0 27939 61 0 0 25 0 1 0 422303328 53518336 12170 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13066 12170 603 41 0 13025 0
vsize: 52264
[startup+289.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13075 0 0 0 28939 61 0 0 25 0 1 0 422303328 53518336 12170 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13066 12170 603 41 0 13025 0
vsize: 52264
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13515 0 0 0 29938 62 0 0 25 0 1 0 422303328 55644160 12549 4294967295 134512640 134672761 3221224560 3221222960 134604097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13585 12549 603 41 0 13544 0
vsize: 54340
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13515 0 0 0 30938 62 0 0 25 0 1 0 422303328 55644160 12549 4294967295 134512640 134672761 3221224560 3221222960 134605448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13585 12549 603 41 0 13544 0
vsize: 54340
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13515 0 0 0 31938 63 0 0 25 0 1 0 422303328 55644160 12549 4294967295 134512640 134672761 3221224560 3221222080 134566687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13585 12549 603 41 0 13544 0
vsize: 54340
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13515 0 0 0 32938 63 0 0 25 0 1 0 422303328 55644160 12549 4294967295 134512640 134672761 3221224560 3221222960 134605448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13585 12549 603 41 0 13544 0
vsize: 54340
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13515 0 0 0 33938 63 0 0 25 0 1 0 422303328 53256192 12109 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13002 12109 603 41 0 12961 0
vsize: 52008
[startup+349.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13515 0 0 0 34938 63 0 0 25 0 1 0 422303328 53256192 12109 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13002 12109 603 41 0 12961 0
vsize: 52008
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 13634 0 0 0 35939 63 0 0 25 0 1 0 422303328 53735424 12228 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13119 12228 603 41 0 13078 0
vsize: 52476
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 16740 0 0 0 36918 84 0 0 25 0 1 0 422303328 62205952 13348 4294967295 134512640 134672761 3221224560 3221223008 134643705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15187 13348 603 41 0 15146 0
vsize: 60748
[startup+380 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 16740 0 0 0 37822 154 0 0 25 0 1 0 422303328 62205952 13348 4294967295 134512640 134672761 3221224560 3221223008 134643777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15187 13348 603 41 0 15146 0
vsize: 60748
[startup+390.001 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 16740 0 0 0 38817 159 0 0 25 0 1 0 422303328 62205952 13348 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15187 13348 603 41 0 15146 0
vsize: 60748
[startup+400.001 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 16740 0 0 0 39817 159 0 0 25 0 1 0 422303328 62205952 13348 4294967295 134512640 134672761 3221224560 3221223008 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15187 13348 603 41 0 15146 0
vsize: 60748
[startup+410.001 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 16740 0 0 0 40816 159 0 0 25 0 1 0 422303328 62205952 13348 4294967295 134512640 134672761 3221224560 3221223040 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15187 13348 603 41 0 15146 0
vsize: 60748
[startup+420.001 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 16740 0 0 0 41816 159 0 0 25 0 1 0 422303328 62205952 13348 4294967295 134512640 134672761 3221224560 3221223008 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15187 13348 603 41 0 15146 0
vsize: 60748
[startup+430.001 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 17164 0 0 0 42815 160 0 0 25 0 1 0 422303328 65400832 13772 4294967295 134512640 134672761 3221224560 3221223056 134606457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15967 13772 603 41 0 15926 0
vsize: 63868
[startup+440.001 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 17164 0 0 0 43816 160 0 0 25 0 1 0 422303328 65400832 13772 4294967295 134512640 134672761 3221224560 3221222960 134604072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15967 13772 603 41 0 15926 0
vsize: 63868
[startup+450.001 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 17164 0 0 0 44815 161 0 0 25 0 1 0 422303328 62205952 13348 4294967295 134512640 134672761 3221224560 3221223008 134643719 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15187 13348 603 41 0 15146 0
vsize: 60748
[startup+460.001 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 17164 0 0 0 45816 161 0 0 25 0 1 0 422303328 62205952 13348 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15187 13348 603 41 0 15146 0
vsize: 60748
[startup+470.001 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 17165 0 0 0 46816 161 0 0 25 0 1 0 422303328 62205952 13349 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15187 13349 603 41 0 15146 0
vsize: 60748
[startup+480.001 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 17643 0 0 0 47815 162 0 0 25 0 1 0 422303328 64290816 13827 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15696 13827 603 41 0 15655 0
vsize: 62784
[startup+490.002 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 18155 0 0 0 48814 163 0 0 25 0 1 0 422303328 66367488 14339 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16203 14339 603 41 0 16162 0
vsize: 64812
[startup+500.002 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 18717 0 0 0 49813 164 0 0 25 0 1 0 422303328 68603904 14901 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16749 14901 603 41 0 16708 0
vsize: 66996
[startup+510.001 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 19492 0 0 0 50811 166 0 0 25 0 1 0 422303328 71745536 15676 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17516 15676 603 41 0 17475 0
vsize: 70064
[startup+520.001 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 19990 0 0 0 51810 167 0 0 25 0 1 0 422303328 73805824 16174 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18019 16174 603 41 0 17978 0
vsize: 72076
[startup+530.002 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 20635 0 0 0 52809 169 0 0 25 0 1 0 422303328 76533760 16819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18685 16819 603 41 0 18644 0
vsize: 74740
[startup+540.002 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 21171 0 0 0 53807 170 0 0 25 0 1 0 422303328 78729216 17355 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19221 17355 603 41 0 19180 0
vsize: 76884
[startup+550.001 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 21654 0 0 0 54806 172 0 0 25 0 1 0 422303328 80695296 17838 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19701 17838 603 41 0 19660 0
vsize: 78804
[startup+560.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 22089 0 0 0 55805 173 0 0 25 0 1 0 422303328 82505728 18273 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20143 18273 603 41 0 20102 0
vsize: 80572
[startup+570.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 22670 0 0 0 56803 175 0 0 25 0 1 0 422303328 84832256 18854 4294967295 134512640 134672761 3221224560 3221223180 134642774 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20711 18854 603 41 0 20670 0
vsize: 82844
[startup+580.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 23225 0 0 0 57802 177 0 0 25 0 1 0 422303328 87150592 19409 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21277 19409 603 41 0 21236 0
vsize: 85108
[startup+590.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 23638 0 0 0 58801 178 0 0 25 0 1 0 422303328 88829952 19822 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21687 19822 603 41 0 21646 0
vsize: 86748
[startup+600.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 24074 0 0 0 59800 179 0 0 25 0 1 0 422303328 90615808 20258 4294967295 134512640 134672761 3221224560 3221223696 134614744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22123 20258 603 41 0 22082 0
vsize: 88492
[startup+610.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 24658 0 0 0 60798 181 0 0 25 0 1 0 422303328 92975104 20842 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22699 20842 603 41 0 22658 0
vsize: 90796
[startup+620.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 25184 0 0 0 61797 182 0 0 25 0 1 0 422303328 95129600 21368 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23225 21368 603 41 0 23184 0
vsize: 92900
[startup+630.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 25750 0 0 0 62796 183 0 0 25 0 1 0 422303328 97456128 21934 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23793 21934 603 41 0 23752 0
vsize: 95172
[startup+640.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 26298 0 0 0 63795 184 0 0 25 0 1 0 422303328 99762176 22482 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24356 22482 603 41 0 24315 0
vsize: 97424
[startup+650.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 26797 0 0 0 64794 185 0 0 25 0 1 0 422303328 101871616 22981 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24871 22981 603 41 0 24830 0
vsize: 99484
[startup+660.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 27408 0 0 0 65792 187 0 0 25 0 1 0 422303328 104337408 23592 4294967295 134512640 134672761 3221224560 3221223568 134607919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25473 23592 603 41 0 25432 0
vsize: 101892
[startup+670.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 28102 0 0 0 66790 189 0 0 25 0 1 0 422303328 107167744 24286 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26164 24286 603 41 0 26123 0
vsize: 104656
[startup+680.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 28646 0 0 0 67788 191 0 0 25 0 1 0 422303328 109342720 24830 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26695 24830 603 41 0 26654 0
vsize: 106780
[startup+690.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 29034 0 0 0 68787 192 0 0 25 0 1 0 422303328 110931968 25218 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27083 25218 603 41 0 27042 0
vsize: 108332
[startup+700.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 29419 0 0 0 69786 193 0 0 25 0 1 0 422303328 112586752 25603 4294967295 134512640 134672761 3221224560 3221223712 134564785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27487 25603 603 41 0 27446 0
vsize: 109948
[startup+710.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 30069 0 0 0 70785 195 0 0 25 0 1 0 422303328 115183616 26253 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28121 26253 603 41 0 28080 0
vsize: 112484
[startup+720.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 30524 0 0 0 71784 195 0 0 25 0 1 0 422303328 117055488 26708 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28578 26708 603 41 0 28537 0
vsize: 114312
[startup+730.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 31063 0 0 0 72783 196 0 0 25 0 1 0 422303328 119263232 27247 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29117 27247 603 41 0 29076 0
vsize: 116468
[startup+740.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 31493 0 0 0 73783 197 0 0 25 0 1 0 422303328 120958976 27677 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29531 27677 603 41 0 29490 0
vsize: 118124
[startup+750.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 31858 0 0 0 74782 198 0 0 25 0 1 0 422303328 122494976 28042 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29906 28042 603 41 0 29865 0
vsize: 119624
[startup+760.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 32524 0 0 0 75781 199 0 0 25 0 1 0 422303328 125222912 28708 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30572 28708 603 41 0 30531 0
vsize: 122288
[startup+770.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 32912 0 0 0 76780 200 0 0 25 0 1 0 422303328 126849024 29096 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30969 29096 603 41 0 30928 0
vsize: 123876
[startup+780.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 33333 0 0 0 77780 200 0 0 25 0 1 0 422303328 128516096 29517 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31376 29517 603 41 0 31335 0
vsize: 125504
[startup+790.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 33709 0 0 0 78780 201 0 0 25 0 1 0 422303328 130097152 29893 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31762 29893 603 41 0 31721 0
vsize: 127048
[startup+800.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 34480 0 0 0 79778 203 0 0 25 0 1 0 422303328 133173248 30664 4294967295 134512640 134672761 3221224560 3221223684 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32513 30664 603 41 0 32472 0
vsize: 130052
[startup+810.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37753 0 0 0 80753 228 0 0 25 0 1 0 422303328 137691136 31476 4294967295 134512640 134672761 3221224560 3221223104 134621238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33616 31476 603 41 0 33575 0
vsize: 134464
[startup+820.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37753 0 0 0 81752 228 0 0 25 0 1 0 422303328 137691136 31476 4294967295 134512640 134672761 3221224560 3221223104 134621359 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33616 31476 603 41 0 33575 0
vsize: 134464
[startup+830.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37753 0 0 0 82742 238 0 0 25 0 1 0 422303328 134561792 31052 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31052 603 41 0 32811 0
vsize: 131408
[startup+840.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37753 0 0 0 83741 238 0 0 25 0 1 0 422303328 134561792 31052 4294967295 134512640 134672761 3221224560 3221223740 134615849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31052 603 41 0 32811 0
vsize: 131408
[startup+850.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37753 0 0 0 84741 238 0 0 25 0 1 0 422303328 134561792 31052 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31052 603 41 0 32811 0
vsize: 131408
[startup+860.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37753 0 0 0 85741 238 0 0 25 0 1 0 422303328 134561792 31052 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31052 603 41 0 32811 0
vsize: 131408
[startup+870.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37753 0 0 0 86741 238 0 0 25 0 1 0 422303328 134561792 31052 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31052 603 41 0 32811 0
vsize: 131408
[startup+880.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37754 0 0 0 87741 238 0 0 25 0 1 0 422303328 134561792 31053 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31053 603 41 0 32811 0
vsize: 131408
[startup+890.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37756 0 0 0 88742 238 0 0 25 0 1 0 422303328 134561792 31055 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31055 603 41 0 32811 0
vsize: 131408
[startup+900.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37758 0 0 0 89742 238 0 0 25 0 1 0 422303328 134561792 31057 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31057 603 41 0 32811 0
vsize: 131408
[startup+910.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37759 0 0 0 90742 238 0 0 25 0 1 0 422303328 134561792 31058 4294967295 134512640 134672761 3221224560 3221223704 134616373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31058 603 41 0 32811 0
vsize: 131408
[startup+920.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37761 0 0 0 91742 238 0 0 25 0 1 0 422303328 134561792 31060 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31060 603 41 0 32811 0
vsize: 131408
[startup+930.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37762 0 0 0 92742 238 0 0 25 0 1 0 422303328 134561792 31061 4294967295 134512640 134672761 3221224560 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31061 603 41 0 32811 0
vsize: 131408
[startup+940.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37764 0 0 0 93742 238 0 0 25 0 1 0 422303328 134561792 31063 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31063 603 41 0 32811 0
vsize: 131408
[startup+950.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37765 0 0 0 94743 238 0 0 25 0 1 0 422303328 134561792 31064 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32852 31064 603 41 0 32811 0
vsize: 131408
[startup+960.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 37766 0 0 0 95743 238 0 0 25 0 1 0 422303328 134823936 31065 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32916 31065 603 41 0 32875 0
vsize: 131664
[startup+970.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 38281 0 0 0 96742 240 0 0 25 0 1 0 422303328 137011200 31580 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33450 31580 603 41 0 33409 0
vsize: 133800
[startup+980.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 38837 0 0 0 97741 241 0 0 25 0 1 0 422303328 139223040 32136 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33990 32136 603 41 0 33949 0
vsize: 135960
[startup+990.003 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 39148 0 0 0 98740 241 0 0 25 0 1 0 422303328 140500992 32447 4294967295 134512640 134672761 3221224560 3221223568 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34302 32447 603 41 0 34261 0
vsize: 137208
[startup+1000 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 39952 0 0 0 99738 244 0 0 25 0 1 0 422303328 143876096 33251 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35126 33251 603 41 0 35085 0
vsize: 140504
[startup+1010 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 40480 0 0 0 100738 244 0 0 25 0 1 0 422303328 145920000 33779 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35625 33779 603 41 0 35584 0
vsize: 142500
[startup+1020 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 40951 0 0 0 101737 245 0 0 25 0 1 0 422303328 147869696 34250 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36101 34250 603 41 0 36060 0
vsize: 144404
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 41626 0 0 0 102736 246 0 0 25 0 1 0 422303328 150708224 34925 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36794 34925 603 41 0 36753 0
vsize: 147176
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 42335 0 0 0 103735 248 0 0 25 0 1 0 422303328 153600000 35634 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37500 35634 603 41 0 37459 0
vsize: 150000
[startup+1050 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 42737 0 0 0 104734 249 0 0 25 0 1 0 422303328 155197440 36036 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37890 36036 603 41 0 37849 0
vsize: 151560
[startup+1060 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 43517 0 0 0 105733 250 0 0 25 0 1 0 422303328 158367744 36816 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38664 36816 603 41 0 38623 0
vsize: 154656
[startup+1070 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 43981 0 0 0 106731 252 0 0 25 0 1 0 422303328 160243712 37280 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39122 37280 603 41 0 39081 0
vsize: 156488
[startup+1080 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 44828 0 0 0 107729 254 0 0 25 0 1 0 422303328 163753984 38127 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39979 38127 603 41 0 39938 0
vsize: 159916
[startup+1090 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 45211 0 0 0 108729 255 0 0 25 0 1 0 422303328 165330944 38510 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40364 38510 603 41 0 40323 0
vsize: 161456
[startup+1100 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 45927 0 0 0 109728 256 0 0 25 0 1 0 422303328 168185856 39226 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41061 39226 603 41 0 41020 0
vsize: 164244
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 46855 0 0 0 110725 258 0 0 25 0 1 0 422303328 172077056 40154 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42011 40154 603 41 0 41970 0
vsize: 168044
[startup+1120 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 50952 0 0 0 111698 286 0 0 25 0 1 0 422303328 176705536 41364 4294967295 134512640 134672761 3221224560 3221223104 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43141 41364 603 41 0 43100 0
vsize: 172564
[startup+1130 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51025 0 0 0 112635 323 0 0 25 0 1 0 422303328 174137344 40898 4294967295 134512640 134672761 3221224560 3221222768 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42514 40898 603 41 0 42473 0
vsize: 170056
[startup+1140 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51036 0 0 0 113618 340 0 0 25 0 1 0 422303328 174137344 40909 4294967295 134512640 134672761 3221224560 3221222976 134631791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42514 40909 603 41 0 42473 0
vsize: 170056
[startup+1150 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51036 0 0 0 114617 340 0 0 25 0 1 0 422303328 174137344 40909 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42514 40909 603 41 0 42473 0
vsize: 170056
[startup+1160 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51036 0 0 0 115617 340 0 0 25 0 1 0 422303328 174137344 40909 4294967295 134512640 134672761 3221224560 3221223008 134643977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42514 40909 603 41 0 42473 0
vsize: 170056
[startup+1170 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51461 0 0 0 116616 341 0 0 25 0 1 0 422303328 177496064 41334 4294967295 134512640 134672761 3221224560 3221222960 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43334 41334 603 41 0 43293 0
vsize: 173336
[startup+1180 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51461 0 0 0 117617 341 0 0 25 0 1 0 422303328 174137344 40910 4294967295 134512640 134672761 3221224560 3221223008 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42514 40910 603 41 0 42473 0
vsize: 170056
[startup+1190 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51461 0 0 0 118617 341 0 0 25 0 1 0 422303328 174137344 40910 4294967295 134512640 134672761 3221224560 3221223816 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42514 40910 603 41 0 42473 0
vsize: 170056
[startup+1200 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51461 0 0 0 119617 341 0 0 25 0 1 0 422303328 174137344 40910 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42514 40910 603 41 0 42473 0
vsize: 170056
[startup+1210 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 2598
Raw data (stat): 2598 (minisat+) R 2597 30854 30853 0 -1 0 51560 0 0 0 120617 342 0 0 25 0 1 0 422303328 174534656 41009 4294967295 134512640 134672761 3221224560 3221223696 134614488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42611 41009 603 41 0 42570 0
vsize: 170444
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.17 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 2598
Raw data (stat): 2598 (minisat+) Z 2597 30854 30853 0 -1 12 51561 0 0 0 120617 358 0 0 25 0 1 0 422303328 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.17
CPU time (s): 1209.76
CPU user time (s): 1206.17
CPU system time (s): 3.58146
CPU usage (%): 99.9658
Max. virtual memory (Kb): 173336
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####