PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb53-24-opb/normalized-frb53-24-2.opb
MD5SUM	45b026c6b351128e9764d865ca917a59
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-40
Optimality of the best value was proved	NO
Number of terms in the objective function	1272
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1272
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1272
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.11
Number of variables	1272
Total number of constraints	94289
Number of constraints which are clauses	94289
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 5634

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        863260 kB
Buffers:         34948 kB
Cached:         116324 kB
SwapCached:        164 kB
Active:          54832 kB
Inactive:        99480 kB
HighTotal:      131008 kB
HighFree:        11060 kB
LowTotal:       903652 kB
LowFree:        852200 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11484 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:25:36 (client local time) WITH STATUS 10 IN 1210.04 SECONDS
stats: 4100 7 1210.04 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94289 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 |   94289   188578 |   28286       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   94289   188578 |   37715       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.87326 s)
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70300     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  169369   364707 |   50810       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/51103          
c   -- var.elim.:  2000/51103          
c   -- var.elim.:  3000/51103          
c   -- var.elim.:  4000/51103          
c   -- var.elim.:  5000/51103          
c   -- var.elim.:  6000/51103          
c   -- var.elim.:  7000/51103          
c   -- var.elim.:  8000/51103          
c   -- var.elim.:  9000/51103          
c   -- var.elim.:  10000/51103          
c   -- var.elim.:  11000/51103          
c   -- var.elim.:  12000/51103          
c   -- var.elim.:  13000/51103          
c   -- var.elim.:  14000/51103          
c   -- var.elim.:  15000/51103          
c   -- var.elim.:  16000/51103          
c   -- var.elim.:  17000/51103          
c   -- var.elim.:  18000/51103          
c   -- var.elim.:  19000/51103          
c   -- var.elim.:  20000/51103          
c   -- var.elim.:  21000/51103          
c   -- var.elim.:  22000/51103          
c   -- var.elim.:  23000/51103          
c   -- var.elim.:  24000/51103          
c   -- var.elim.:  25000/51103          
c   -- var.elim.:  26000/51103          
c   -- var.elim.:  27000/51103          
c   -- var.elim.:  28000/51103          
c   -- var.elim.:  29000/51103          
c   -- var.elim.:  30000/51103          
c   -- var.elim.:  31000/51103          
c   -- var.elim.:  32000/51103          
c   -- var.elim.:  33000/51103          
c   -- var.elim.:  34000/51103          
c   -- var.elim.:  35000/51103          
c   -- var.elim.:  36000/51103          
c   -- var.elim.:  37000/51103          
c   -- var.elim.:  38000/51103          
c   -- var.elim.:  39000/51103          
c   -- var.elim.:  40000/51103          
c   -- var.elim.:  41000/51103          
c   -- var.elim.:  42000/51103          
c   -- var.elim.:  43000/51103          
c   -- var.elim.:  44000/51103          
c   -- var.elim.:  45000/51103          
c   -- var.elim.:  46000/51103          
c   -- var.elim.:  47000/51103          
c   -- var.elim.:  48000/51103          
c   -- var.elim.:  49000/51103          
c   -- var.elim.:  50000/51103          
c   -- var.elim.:  51000/51103          
c   -- var.elim.:  51103/51103          
c   -- var.elim.:  1000/25897          
c   -- var.elim.:  2000/25897          
c   -- var.elim.:  3000/25897          
c   -- var.elim.:  4000/25897          
c   -- var.elim.:  5000/25897          
c   -- var.elim.:  6000/25897          
c   -- var.elim.:  7000/25897          
c   -- var.elim.:  8000/25897          
c   -- var.elim.:  9000/25897          
c   -- var.elim.:  10000/25897          
c   -- var.elim.:  11000/25897          
c   -- var.elim.:  12000/25897          
c   -- var.elim.:  13000/25897          
c   -- var.elim.:  14000/25897          
c   -- var.elim.:  15000/25897          
c   -- var.elim.:  16000/25897          
c   -- var.elim.:  17000/25897          
c   -- var.elim.:  18000/25897          
c   -- var.elim.:  19000/25897          
c   -- var.elim.:  20000/25897          
c   -- var.elim.:  21000/25897          
c   -- var.elim.:  22000/25897          
c   -- var.elim.:  23000/25897          
c   -- var.elim.:  24000/25897          
c   -- var.elim.:  25000/25897          
c   -- var.elim.:  25897/25897          
c   -- var.elim.:  298/298          
c   -- var.elim.:  133/133          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  1000/9592          
c   -- var.elim.:  2000/9592          
c   -- var.elim.:  3000/9592          
c   -- var.elim.:  4000/9592          
c   -- var.elim.:  5000/9592          
c   -- var.elim.:  6000/9592          
c   -- var.elim.:  7000/9592          
c   -- var.elim.:  8000/9592          
c   -- var.elim.:  9000/9592          
c   -- var.elim.:  9592/9592          
c   -- var.elim.:  425/425          
c |         0 |  114661   370453 |      --       0       --      -- |     --   | -54702/5764
c |         0 |  114661   370453 |   45864       0        0     nan |  0.000 % |
c |       100 |  114661   370453 |   50450     100    10876   108.8 | 56.447 % |
c |       250 |  114661   370453 |   55495     250    36249   145.0 | 56.447 % |
c |       475 |  114661   370453 |   61045     475    63686   134.1 | 56.447 % |
c |       812 |  114661   370453 |   67150     812   131964   162.5 | 56.447 % |
c |      1318 |  114661   370453 |   73865    1318   209228   158.7 | 56.447 % |
c |      2077 |  114661   370453 |   81251    2077   334633   161.1 | 56.447 % |
c |      3216 |  114629   370085 |   89351    3210   560710   174.7 | 56.509 % |
c |      4924 |  114629   370085 |   98286    4918  1023652   208.1 | 56.509 % |
c |      7486 |  114559   369379 |  108049    7468  1581097   211.7 | 56.644 % |
c |     11331 |  114323   367208 |  118609   11290  2464334   218.3 | 57.101 % |
c |     17097 |  113867   362928 |  129950   16973  3919442   230.9 | 57.985 % |
c |     25746 |  113355   358317 |  142302   25539  6447796   252.5 | 58.976 % |
c ==============================================================================
c (current CPU-time: 414.334 s)
c ==============================================================================
c [1mFound solution: -39[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 |     35056 |  122336   377655 |   36700   34740  9535324   274.5 | 58.976 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18561          
c   -- var.elim.:  2000/18561          
c   -- var.elim.:  3000/18561          
c   -- var.elim.:  4000/18561          
c   -- var.elim.:  5000/18561          
c   -- var.elim.:  6000/18561          
c   -- var.elim.:  7000/18561          
c   -- var.elim.:  8000/18561          
c   -- var.elim.:  9000/18561          
c   -- var.elim.:  10000/18561          
c   -- var.elim.:  11000/18561          
c   -- var.elim.:  12000/18561          
c   -- var.elim.:  13000/18561          
c   -- var.elim.:  14000/18561          
c   -- var.elim.:  15000/18561          
c   -- var.elim.:  16000/18561          
c   -- var.elim.:  17000/18561          
c   -- var.elim.:  18000/18561          
c   -- var.elim.:  18561/18561          
c   -- var.elim.:  1000/6780          
c   -- var.elim.:  2000/6780          
c   -- var.elim.:  3000/6780          
c   -- var.elim.:  4000/6780          
c   -- var.elim.:  5000/6780          
c   -- var.elim.:  6000/6780          
c   -- var.elim.:  6780/6780          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  1000/6673          
c   -- var.elim.:  2000/6673          
c   -- var.elim.:  3000/6673          
c   -- var.elim.:  4000/6673          
c   -- var.elim.:  5000/6673          
c   -- var.elim.:  6000/6673          
c   -- var.elim.:  6673/6673          
c   -- var.elim.:  95/95          
c |     35056 |  112733   362007 |      --   34740       --      -- |     --   | -9594/-15629
c |     35056 |  112733   362007 |   45093   34124  9203278   269.7 | 58.976 % |
c |     35156 |  112733   362007 |   49602   34224  9218051   269.3 | 68.282 % |
c |     35306 |  112733   362007 |   54562   34374  9320065   271.1 | 68.282 % |
c ==============================================================================
c (current CPU-time: 486.349 s)
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     35352 |  114694   366784 |   34408   34401  9325246   271.1 | 68.282 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10188          
c   -- var.elim.:  2000/10188          
c   -- var.elim.:  3000/10188          
c   -- var.elim.:  4000/10188          
c   -- var.elim.:  5000/10188          
c   -- var.elim.:  6000/10188          
c   -- var.elim.:  7000/10188          
c   -- var.elim.:  8000/10188          
c   -- var.elim.:  9000/10188          
c   -- var.elim.:  10000/10188          
c   -- var.elim.:  10188/10188          
c   -- var.elim.:  1000/1998          
c   -- var.elim.:  1998/1998          
c |     35352 |  112623   361381 |      --   34401       --      -- |     --   | -2054/-2944
c |     35352 |  112623   361381 |   45049   34401  9325246   271.1 | 68.282 % |
c |     35453 |  112623   361381 |   49554   34502  9366574   271.5 | 68.520 % |
c |     35603 |  112623   361381 |   54509   34652  9409074   271.5 | 68.520 % |
c |     35828 |  112623   361381 |   59960   34877  9471193   271.6 | 68.520 % |
c |     36166 |  112623   361381 |   65956   35215  9580011   272.0 | 68.520 % |
c |     36672 |  112549   360737 |   72504   35557  9543715   268.4 | 68.634 % |
c |     37433 |  112511   360387 |   79728   36306  9762017   268.9 | 68.693 % |
c |     38572 |  112487   360133 |   87682   37444 10105739   269.9 | 68.730 % |
c |     40280 |  112303   358336 |   96292   39115 10539913   269.5 | 69.014 % |
c |     42842 |  111920   354701 |  105560   41603 11330348   272.3 | 69.589 % |
c |     46687 |  111666   352196 |  115853   45334 12512166   276.0 | 69.970 % |
c |     52453 |  111215   347797 |  126923   50984 14373111   281.9 | 70.638 % |
c |     61102 |  109917   335148 |  137986   59398 17244763   290.3 | 72.616 % |
c |     74076 |  109277   328841 |  150901   72085 21564972   299.2 | 73.581 % |
c |     93537 |  108490   321151 |  164796   91175 28392677   311.4 | 74.771 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 C889 -C888 -C887 -C886 -C885 C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 C650 -C649 -C648 -C647 -C646 C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -#### 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.92 0.99 0.93 2/54 30793
Raw data (stat): 30793 (runsolver) R 30792 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422279746 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.99 0.93 2/54 30793
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10236 0 0 0 950 48 0 0 25 0 1 0 422279746 44494848 9645 4294967295 134512640 134672761 3221224560 3221222976 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10863 9645 603 41 0 10822 0
vsize: 43452
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.99 0.93 2/54 30793
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10476 0 0 0 1948 50 0 0 25 0 1 0 422279746 45387776 9885 4294967295 134512640 134672761 3221224560 3221222992 134605682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11081 9885 603 41 0 11040 0
vsize: 44324
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.99 0.93 2/54 30793
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10477 0 0 0 2948 50 0 0 25 0 1 0 422279746 45387776 9886 4294967295 134512640 134672761 3221224560 3221222816 134621573 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11081 9886 603 41 0 11040 0
vsize: 44324
[startup+40.0017 s]
Raw data (loadavg): 0.96 0.99 0.93 2/54 30793
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10478 0 0 0 3947 50 0 0 25 0 1 0 422279746 45387776 9887 4294967295 134512640 134672761 3221224560 3221223056 134644260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11081 9887 603 41 0 11040 0
vsize: 44324
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10479 0 0 0 4948 50 0 0 25 0 1 0 422279746 45387776 9888 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11081 9888 603 41 0 11040 0
vsize: 44324
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10480 0 0 0 5948 50 0 0 25 0 1 0 422279746 45387776 9889 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11081 9889 603 41 0 11040 0
vsize: 44324
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10485 0 0 0 6948 50 0 0 25 0 1 0 422279746 45387776 9894 4294967295 134512640 134672761 3221224560 3221223088 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11081 9894 603 41 0 11040 0
vsize: 44324
[startup+80.0022 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10518 0 0 0 7948 50 0 0 25 0 1 0 422279746 45649920 9927 4294967295 134512640 134672761 3221224560 3221223056 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11145 9927 603 41 0 11104 0
vsize: 44580
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10519 0 0 0 8948 50 0 0 25 0 1 0 422279746 45649920 9928 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11145 9928 603 41 0 11104 0
vsize: 44580
[startup+100.002 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10520 0 0 0 9948 50 0 0 25 0 1 0 422279746 45649920 9929 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11145 9929 603 41 0 11104 0
vsize: 44580
[startup+110.002 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10521 0 0 0 10949 50 0 0 25 0 1 0 422279746 45649920 9930 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11145 9930 603 41 0 11104 0
vsize: 44580
[startup+120.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10524 0 0 0 11949 50 0 0 25 0 1 0 422279746 45649920 9933 4294967295 134512640 134672761 3221224560 3221223088 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11145 9933 603 41 0 11104 0
vsize: 44580
[startup+130.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10525 0 0 0 12949 50 0 0 25 0 1 0 422279746 45649920 9934 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11145 9934 603 41 0 11104 0
vsize: 44580
[startup+140.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10527 0 0 0 13949 50 0 0 25 0 1 0 422279746 45649920 9936 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11145 9936 603 41 0 11104 0
vsize: 44580
[startup+150.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10528 0 0 0 14949 50 0 0 25 0 1 0 422279746 45649920 9937 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11145 9937 603 41 0 11104 0
vsize: 44580
[startup+160.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10541 0 0 0 15949 50 0 0 25 0 1 0 422279746 45879296 9950 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11201 9950 603 41 0 11160 0
vsize: 44804
[startup+170.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10544 0 0 0 16950 50 0 0 25 0 1 0 422279746 45879296 9953 4294967295 134512640 134672761 3221224560 3221222816 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11201 9953 603 41 0 11160 0
vsize: 44804
[startup+180.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10548 0 0 0 17950 50 0 0 25 0 1 0 422279746 45879296 9957 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11201 9957 603 41 0 11160 0
vsize: 44804
[startup+190.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10553 0 0 0 18950 50 0 0 25 0 1 0 422279746 45879296 9962 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11201 9962 603 41 0 11160 0
vsize: 44804
[startup+200.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10557 0 0 0 19950 50 0 0 25 0 1 0 422279746 45879296 9966 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11201 9966 603 41 0 11160 0
vsize: 44804
[startup+210.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10557 0 0 0 20950 50 0 0 25 0 1 0 422279746 45879296 9966 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11201 9966 603 41 0 11160 0
vsize: 44804
[startup+220.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10889 0 0 0 21948 51 0 0 25 0 1 0 422279746 48353280 10298 4294967295 134512640 134672761 3221224560 3221223032 134644217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11805 10298 603 41 0 11764 0
vsize: 47220
[startup+230.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10889 0 0 0 22948 51 0 0 25 0 1 0 422279746 48353280 10298 4294967295 134512640 134672761 3221224560 3221222960 134605448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11805 10298 603 41 0 11764 0
vsize: 47220
[startup+240.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10889 0 0 0 23948 51 0 0 25 0 1 0 422279746 48353280 10298 4294967295 134512640 134672761 3221224560 3221223052 134642887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11805 10298 603 41 0 11764 0
vsize: 47220
[startup+250.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10889 0 0 0 24949 51 0 0 25 0 1 0 422279746 48353280 10298 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11805 10298 603 41 0 11764 0
vsize: 47220
[startup+260.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10889 0 0 0 25949 51 0 0 25 0 1 0 422279746 45879296 9966 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11201 9966 603 41 0 11160 0
vsize: 44804
[startup+270.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 10899 0 0 0 26949 51 0 0 25 0 1 0 422279746 45879296 9976 4294967295 134512640 134672761 3221224560 3221223712 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11201 9976 603 41 0 11160 0
vsize: 44804
[startup+280.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 11573 0 0 0 27948 52 0 0 25 0 1 0 422279746 48570368 10650 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11858 10650 603 41 0 11817 0
vsize: 47432
[startup+290.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 12218 0 0 0 28947 54 0 0 25 0 1 0 422279746 51183616 11295 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12496 11295 603 41 0 12455 0
vsize: 49984
[startup+300.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 12908 0 0 0 29946 55 0 0 25 0 1 0 422279746 54071296 11985 4294967295 134512640 134672761 3221224560 3221223684 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13201 11985 603 41 0 13160 0
vsize: 52804
[startup+310.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 13524 0 0 0 30944 57 0 0 25 0 1 0 422279746 56561664 12601 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13809 12601 603 41 0 13768 0
vsize: 55236
[startup+320.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 14172 0 0 0 31943 58 0 0 25 0 1 0 422279746 59330560 13249 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14485 13249 603 41 0 14444 0
vsize: 57940
[startup+330.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 14754 0 0 0 32942 60 0 0 25 0 1 0 422279746 61681664 13831 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15059 13831 603 41 0 15018 0
vsize: 60236
[startup+340.004 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 15483 0 0 0 33940 62 0 0 25 0 1 0 422279746 64655360 14560 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15785 14560 603 41 0 15744 0
vsize: 63140
[startup+350.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 16148 0 0 0 34939 63 0 0 25 0 1 0 422279746 67309568 15225 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16433 15225 603 41 0 16392 0
vsize: 65732
[startup+360.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 16695 0 0 0 35938 64 0 0 25 0 1 0 422279746 69619712 15772 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16997 15772 603 41 0 16956 0
vsize: 67988
[startup+370.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 17175 0 0 0 36937 66 0 0 25 0 1 0 422279746 71569408 16252 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17473 16252 603 41 0 17432 0
vsize: 69892
[startup+380.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 17664 0 0 0 37935 67 0 0 25 0 1 0 422279746 73531392 16741 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17952 16741 603 41 0 17911 0
vsize: 71808
[startup+390.004 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 18206 0 0 0 38934 68 0 0 25 0 1 0 422279746 75718656 17283 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18486 17283 603 41 0 18445 0
vsize: 73944
[startup+400.004 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 18883 0 0 0 39933 70 0 0 25 0 1 0 422279746 78548992 17960 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19177 17960 603 41 0 19136 0
vsize: 76708
[startup+410.004 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 19580 0 0 0 40931 72 0 0 25 0 1 0 422279746 81534976 18657 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19906 18657 603 41 0 19865 0
vsize: 79624
[startup+420.004 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 22170 0 0 0 41921 82 0 0 25 0 1 0 422279746 91639808 20022 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22373 20022 603 41 0 22332 0
vsize: 89492
[startup+430.004 s]
Raw data (loadavg): 0.99 0.99 0.93 1/54 30795
Raw data (stat): 30793 (minisat+) D 30792 25347 25346 0 -1 0 22170 0 0 0 42866 116 0 0 25 0 1 0 422279746 89845760 19690 4294967295 134512640 134672761 3221224560 3221222768 1075730206 0 0 5 16386 3222661533 0 0 17 0 0 0
Raw data (statm): 21935 19690 603 41 0 21894 0
vsize: 87740
[startup+440.005 s]
Raw data (loadavg): 1.07 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 22170 0 0 0 43836 141 0 0 25 0 1 0 422279746 89845760 19690 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21935 19690 603 41 0 21894 0
vsize: 87740
[startup+450.004 s]
Raw data (loadavg): 1.06 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 22170 0 0 0 44836 141 0 0 25 0 1 0 422279746 89845760 19690 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21935 19690 603 41 0 21894 0
vsize: 87740
[startup+460.003 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 22170 0 0 0 45836 141 0 0 25 0 1 0 422279746 89845760 19690 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21935 19690 603 41 0 21894 0
vsize: 87740
[startup+470.004 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 22502 0 0 0 46835 142 0 0 25 0 1 0 422279746 92418048 20022 4294967295 134512640 134672761 3221224560 3221223104 134621060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22563 20022 603 41 0 22522 0
vsize: 90252
[startup+480.003 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 22502 0 0 0 47835 142 0 0 25 0 1 0 422279746 89845760 19690 4294967295 134512640 134672761 3221224560 3221223008 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21935 19690 603 41 0 21894 0
vsize: 87740
[startup+490.003 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 24886 0 0 0 48813 163 0 0 25 0 1 0 422279746 92438528 20064 4294967295 134512640 134672761 3221224560 3221223104 134621202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22568 20064 603 41 0 22527 0
vsize: 90272
[startup+500.004 s]
Raw data (loadavg): 1.10 1.02 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 24886 0 0 0 49806 172 0 0 25 0 1 0 422279746 89841664 19732 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21934 19732 603 41 0 21893 0
vsize: 87736
[startup+510.004 s]
Raw data (loadavg): 1.09 1.02 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 24886 0 0 0 50805 172 0 0 25 0 1 0 422279746 89841664 19732 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21934 19732 603 41 0 21893 0
vsize: 87736
[startup+520.004 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 24908 0 0 0 51806 172 0 0 25 0 1 0 422279746 89972736 19754 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21966 19754 603 41 0 21925 0
vsize: 87864
[startup+530.004 s]
Raw data (loadavg): 1.06 1.02 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 25434 0 0 0 52805 173 0 0 25 0 1 0 422279746 92078080 20280 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22480 20280 603 41 0 22439 0
vsize: 89920
[startup+540.004 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 25791 0 0 0 53805 173 0 0 25 0 1 0 422279746 93655040 20637 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22865 20637 603 41 0 22824 0
vsize: 91460
[startup+550.003 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 26298 0 0 0 54804 174 0 0 25 0 1 0 422279746 95694848 21144 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23363 21144 603 41 0 23322 0
vsize: 93452
[startup+560.003 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 26706 0 0 0 55803 175 0 0 25 0 1 0 422279746 97263616 21552 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23746 21552 603 41 0 23705 0
vsize: 94984
[startup+570.004 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 27127 0 0 0 56803 176 0 0 25 0 1 0 422279746 98979840 21973 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24165 21973 603 41 0 24124 0
vsize: 96660
[startup+580.003 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 27736 0 0 0 57801 177 0 0 25 0 1 0 422279746 101588992 22582 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24802 22582 603 41 0 24761 0
vsize: 99208
[startup+590.004 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 28284 0 0 0 58800 178 0 0 25 0 1 0 422279746 103780352 23130 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25337 23130 603 41 0 25296 0
vsize: 101348
[startup+600.003 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 28660 0 0 0 59800 179 0 0 25 0 1 0 422279746 105299968 23506 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25708 23506 603 41 0 25667 0
vsize: 102832
[startup+610.003 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 29036 0 0 0 60799 180 0 0 25 0 1 0 422279746 106872832 23882 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26092 23882 603 41 0 26051 0
vsize: 104368
[startup+620.003 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 29404 0 0 0 61798 181 0 0 25 0 1 0 422279746 108290048 24250 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26438 24250 603 41 0 26397 0
vsize: 105752
[startup+630.003 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 29983 0 0 0 62797 182 0 0 25 0 1 0 422279746 110718976 24829 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27031 24829 603 41 0 26990 0
vsize: 108124
[startup+640.004 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 30569 0 0 0 63797 183 0 0 25 0 1 0 422279746 113090560 25415 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27610 25415 603 41 0 27569 0
vsize: 110440
[startup+650.003 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 30932 0 0 0 64796 184 0 0 25 0 1 0 422279746 114524160 25778 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27960 25778 603 41 0 27919 0
vsize: 111840
[startup+660.003 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 31288 0 0 0 65795 185 0 0 25 0 1 0 422279746 116076544 26134 4294967295 134512640 134672761 3221224560 3221223408 134604097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28339 26134 603 41 0 28298 0
vsize: 113356
[startup+670.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 31651 0 0 0 66795 186 0 0 25 0 1 0 422279746 117547008 26497 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28698 26497 603 41 0 28657 0
vsize: 114792
[startup+680.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 32079 0 0 0 67793 187 0 0 25 0 1 0 422279746 119316480 26925 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29130 26925 603 41 0 29089 0
vsize: 116520
[startup+690.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 32836 0 0 0 68792 188 0 0 25 0 1 0 422279746 122417152 27682 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29887 27682 603 41 0 29846 0
vsize: 119548
[startup+700.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 33233 0 0 0 69792 189 0 0 25 0 1 0 422279746 123985920 28079 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30270 28079 603 41 0 30229 0
vsize: 121080
[startup+710.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 33761 0 0 0 70791 190 0 0 25 0 1 0 422279746 126189568 28607 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30808 28607 603 41 0 30767 0
vsize: 123232
[startup+720.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 34105 0 0 0 71790 191 0 0 25 0 1 0 422279746 127483904 28951 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31124 28951 603 41 0 31083 0
vsize: 124496
[startup+730.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 34490 0 0 0 72789 192 0 0 25 0 1 0 422279746 129052672 29336 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31507 29336 603 41 0 31466 0
vsize: 126028
[startup+740.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 34881 0 0 0 73789 193 0 0 25 0 1 0 422279746 130969600 29727 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31975 29727 603 41 0 31934 0
vsize: 127900
[startup+750.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 35226 0 0 0 74788 194 0 0 25 0 1 0 422279746 132403200 30072 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32325 30072 603 41 0 32284 0
vsize: 129300
[startup+760.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 35514 0 0 0 75787 195 0 0 25 0 1 0 422279746 133578752 30360 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32612 30360 603 41 0 32571 0
vsize: 130448
[startup+770.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 35920 0 0 0 76786 196 0 0 25 0 1 0 422279746 135254016 30766 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33021 30766 603 41 0 32980 0
vsize: 132084
[startup+780.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 36271 0 0 0 77785 197 0 0 25 0 1 0 422279746 136691712 31117 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33372 31117 603 41 0 33331 0
vsize: 133488
[startup+790.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 36719 0 0 0 78785 198 0 0 25 0 1 0 422279746 138530816 31565 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33821 31565 603 41 0 33780 0
vsize: 135284
[startup+800.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 37103 0 0 0 79784 199 0 0 25 0 1 0 422279746 140083200 31949 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34200 31949 603 41 0 34159 0
vsize: 136800
[startup+810.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 37567 0 0 0 80783 200 0 0 25 0 1 0 422279746 141905920 32413 4294967295 134512640 134672761 3221224560 3221223696 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34645 32413 603 41 0 34604 0
vsize: 138580
[startup+820.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 38144 0 0 0 81782 201 0 0 25 0 1 0 422279746 144240640 32990 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35215 32990 603 41 0 35174 0
vsize: 140860
[startup+830.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 38325 0 0 0 82781 202 0 0 25 0 1 0 422279746 145031168 33171 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35408 33171 603 41 0 35367 0
vsize: 141632
[startup+840.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 38728 0 0 0 83781 203 0 0 25 0 1 0 422279746 146735104 33574 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35824 33574 603 41 0 35783 0
vsize: 143296
[startup+850.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 39187 0 0 0 84779 205 0 0 25 0 1 0 422279746 148574208 34033 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36273 34033 603 41 0 36232 0
vsize: 145092
[startup+860.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 39649 0 0 0 85778 206 0 0 25 0 1 0 422279746 150474752 34495 4294967295 134512640 134672761 3221224560 3221223600 134612885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36737 34495 603 41 0 36696 0
vsize: 146948
[startup+870.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 40028 0 0 0 86777 207 0 0 25 0 1 0 422279746 152043520 34874 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37120 34874 603 41 0 37079 0
vsize: 148480
[startup+880.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 40395 0 0 0 87776 208 0 0 25 0 1 0 422279746 153440256 35241 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37461 35241 603 41 0 37420 0
vsize: 149844
[startup+890.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 41051 0 0 0 88776 209 0 0 25 0 1 0 422279746 156209152 35897 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38137 35897 603 41 0 38096 0
vsize: 152548
[startup+900.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 41330 0 0 0 89775 210 0 0 25 0 1 0 422279746 157249536 36176 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38391 36176 603 41 0 38350 0
vsize: 153564
[startup+910.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 41653 0 0 0 90775 210 0 0 25 0 1 0 422279746 158625792 36499 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38727 36499 603 41 0 38686 0
vsize: 154908
[startup+920.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 42141 0 0 0 91774 211 0 0 25 0 1 0 422279746 160649216 36987 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39221 36987 603 41 0 39180 0
vsize: 156884
[startup+930.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 42518 0 0 0 92774 212 0 0 25 0 1 0 422279746 162213888 37364 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39603 37364 603 41 0 39562 0
vsize: 158412
[startup+940.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 42907 0 0 0 93773 213 0 0 25 0 1 0 422279746 163741696 37753 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39976 37753 603 41 0 39935 0
vsize: 159904
[startup+950.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 43314 0 0 0 94772 213 0 0 25 0 1 0 422279746 165421056 38160 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40386 38160 603 41 0 40345 0
vsize: 161544
[startup+960.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 43846 0 0 0 95772 214 0 0 25 0 1 0 422279746 167563264 38692 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40909 38692 603 41 0 40868 0
vsize: 163636
[startup+970.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 44026 0 0 0 96772 215 0 0 25 0 1 0 422279746 168321024 38872 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41094 38872 603 41 0 41053 0
vsize: 164376
[startup+980.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 44578 0 0 0 97771 216 0 0 25 0 1 0 422279746 170631168 39424 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41658 39424 603 41 0 41617 0
vsize: 166632
[startup+990.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 45136 0 0 0 98770 217 0 0 25 0 1 0 422279746 172797952 39982 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42187 39982 603 41 0 42146 0
vsize: 168748
[startup+1000 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 45594 0 0 0 99768 218 0 0 25 0 1 0 422279746 174714880 40440 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42655 40440 603 41 0 42614 0
vsize: 170620
[startup+1010 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 46087 0 0 0 100768 219 0 0 25 0 1 0 422279746 176795648 40933 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43163 40933 603 41 0 43122 0
vsize: 172652
[startup+1020 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 46585 0 0 0 101767 220 0 0 25 0 1 0 422279746 178753536 41431 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43641 41431 603 41 0 43600 0
vsize: 174564
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 46756 0 0 0 102767 220 0 0 25 0 1 0 422279746 179531776 41602 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43831 41602 603 41 0 43790 0
vsize: 175324
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 47193 0 0 0 103766 221 0 0 25 0 1 0 422279746 181321728 42039 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44268 42039 603 41 0 44227 0
vsize: 177072
[startup+1050 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 47714 0 0 0 104765 222 0 0 25 0 1 0 422279746 183427072 42560 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44782 42560 603 41 0 44741 0
vsize: 179128
[startup+1060 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 48159 0 0 0 105764 224 0 0 25 0 1 0 422279746 185233408 43005 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45223 43005 603 41 0 45182 0
vsize: 180892
[startup+1070 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 48414 0 0 0 106764 224 0 0 25 0 1 0 422279746 186277888 43260 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45478 43260 603 41 0 45437 0
vsize: 181912
[startup+1080 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 48693 0 0 0 107763 226 0 0 25 0 1 0 422279746 187449344 43539 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45764 43539 603 41 0 45723 0
vsize: 183056
[startup+1090 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 48955 0 0 0 108762 226 0 0 25 0 1 0 422279746 188497920 43801 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46020 43801 603 41 0 45979 0
vsize: 184080
[startup+1100 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 49350 0 0 0 109762 227 0 0 25 0 1 0 422279746 190062592 44196 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46402 44196 603 41 0 46361 0
vsize: 185608
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 50044 0 0 0 110761 228 0 0 25 0 1 0 422279746 192876544 44890 4294967295 134512640 134672761 3221224560 3221223600 134612885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47089 44890 603 41 0 47048 0
vsize: 188356
[startup+1120 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 50452 0 0 0 111760 229 0 0 25 0 1 0 422279746 194588672 45298 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47507 45298 603 41 0 47466 0
vsize: 190028
[startup+1130 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 50975 0 0 0 112759 230 0 0 25 0 1 0 422279746 196775936 45821 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48041 45821 603 41 0 48000 0
vsize: 192164
[startup+1140 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 51209 0 0 0 113758 231 0 0 25 0 1 0 422279746 197660672 46055 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48257 46055 603 41 0 48216 0
vsize: 193028
[startup+1150 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 51592 0 0 0 114756 232 0 0 25 0 1 0 422279746 199294976 46438 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48656 46438 603 41 0 48615 0
vsize: 194624
[startup+1160 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 52089 0 0 0 115755 233 0 0 25 0 1 0 422279746 201240576 46935 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49131 46935 603 41 0 49090 0
vsize: 196524
[startup+1170 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 52381 0 0 0 116755 233 0 0 25 0 1 0 422279746 202518528 47227 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49443 47227 603 41 0 49402 0
vsize: 197772
[startup+1180 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 52919 0 0 0 117754 234 0 0 25 0 1 0 422279746 204611584 47765 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49954 47765 603 41 0 49913 0
vsize: 199816
[startup+1190 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 53510 0 0 0 118753 236 0 0 25 0 1 0 422279746 207036416 48356 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50546 48356 603 41 0 50505 0
vsize: 202184
[startup+1200 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 53993 0 0 0 119752 237 0 0 25 0 1 0 422279746 208998400 48839 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51025 48839 603 41 0 50984 0
vsize: 204100
[startup+1210 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30795
Raw data (stat): 30793 (minisat+) R 30792 25347 25346 0 -1 0 54250 0 0 0 120752 237 0 0 25 0 1 0 422279746 210051072 49096 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51282 49096 603 41 0 51241 0
vsize: 205128
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.14 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 30795
Raw data (stat): 30793 (minisat+) Z 30792 25347 25346 0 -1 12 54251 0 0 0 120752 251 0 0 25 0 1 0 422279746 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.14
CPU time (s): 1210.04
CPU user time (s): 1207.53
CPU system time (s): 2.51062
CPU usage (%): 99.9912
Max. virtual memory (Kb): 205128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####