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/frb45-21-opb/normalized-frb45-21-3.opb
MD5SUM	b3a3f977e810fc2043ea057a8d94a7d8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-34
Optimality of the best value was proved	NO
Number of terms in the objective function	945
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	945
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	945
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.07
Number of variables	945
Total number of constraints	58245
Number of constraints which are clauses	58245
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 6376

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        811936 kB
Buffers:         36864 kB
Cached:         147812 kB
SwapCached:         12 kB
Active:          66764 kB
Inactive:       120808 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        811684 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29304 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:03:48 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 4843 7 1200.37 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58245 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   58245   116490 |   19415       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  149606   330344 |   49868       0        0     nan |  0.000 % |
c |       101 |  149034   329045 |   54854      81      599     7.4 |  0.608 % |
c |       251 |  147252   324967 |   60340     191     1152     6.0 |  2.260 % |
c |       476 |  144011   317537 |   66374     350     2037     5.8 |  5.437 % |
c |       813 |  138960   305943 |   73011     563     3544     6.3 | 10.423 % |
c |      1320 |  134550   295791 |   80312     944     6854     7.3 | 15.344 % |
c |      2079 |  125057   273752 |   88344    1377    12968     9.4 | 24.521 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2714 |  119978   261981 |   39992    1810    15834     8.7 | 24.521 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2741 |  119821   261751 |   39940    1811    15829     8.7 | 24.521 % |
c |      2841 |  119558   261146 |   43934    1903    17821     9.4 | 30.696 % |
c |      2991 |  117804   257114 |   48327    2017    18854     9.3 | 32.432 % |
c |      3216 |  116126   253226 |   53160    2197    19801     9.0 | 34.165 % |
c |      3553 |  113977   248244 |   58476    2464    22746     9.2 | 36.395 % |
c |      4059 |  111878   243382 |   64323    2869    26154     9.1 | 38.580 % |
c |      4818 |  106013   229751 |   70756    3342    33180     9.9 | 44.705 % |
c |      5957 |   99224   213776 |   77831    4079    40334     9.9 | 52.063 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6785 |   96589   207731 |   32196    4731    47917    10.1 | 52.063 % |
c |      6885 |   95996   206345 |   35415    4789    48278    10.1 | 55.703 % |
c |      7035 |   95603   205427 |   38957    4921    49839    10.1 | 56.127 % |
c |      7260 |   94710   203336 |   42852    5056    51692    10.2 | 57.120 % |
c |      7597 |   93991   201658 |   47138    5334    53559    10.0 | 57.924 % |
c |      8103 |   90121   192639 |   51851    5400    55135    10.2 | 62.026 % |
c |      8862 |   87106   185518 |   57037    5767    61201    10.6 | 65.330 % |
c |     10001 |   84934   180423 |   62740    6667    75142    11.3 | 67.651 % |
c |     11710 |   79805   168389 |   69014    7564    97042    12.8 | 73.263 % |
c |     14272 |   75515   158269 |   75916    9123   137854    15.1 | 78.128 % |
c |     18117 |   73358   153181 |   83508   12062   264157    21.9 | 80.512 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20637 |   72888   152031 |   24296   14260   382200    26.8 | 80.512 % |
c |     20737 |   72599   151359 |   26725   14283   382672    26.8 | 81.327 % |
c |     20888 |   72599   151359 |   29398   14434   388281    26.9 | 81.327 % |
c |     21113 |   72599   151359 |   32337   14659   401792    27.4 | 81.327 % |
c |     21450 |   72589   151336 |   35571   14995   418069    27.9 | 81.337 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21858 |   72619   151423 |   24206   15381   443751    28.9 | 81.337 % |
c |     21958 |   72613   151409 |   26626   15480   445030    28.7 | 81.342 % |
c |     22110 |   72613   151409 |   29289   15632   448328    28.7 | 81.342 % |
c |     22335 |   72613   151409 |   32218   15857   453089    28.6 | 81.342 % |
c |     22672 |   72613   151409 |   35440   16194   469930    29.0 | 81.342 % |
c |     23178 |   72607   151395 |   38984   16698   486905    29.2 | 81.348 % |
c |     23937 |   71504   148771 |   42882   17088   519243    30.4 | 82.630 % |
c |     25076 |   71417   148569 |   47170   18110   598910    33.1 | 82.723 % |
c |     26784 |   71074   147760 |   51887   19432   634957    32.7 | 83.124 % |
c |     29347 |   70666   146798 |   57076   21630   854526    39.5 | 83.600 % |
c |     33191 |   70203   145701 |   62784   25105  1192310    47.5 | 84.123 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38533 |   70021   145225 |   23340   30156  1729105    57.3 | 84.123 % |
c |     38635 |   70021   145225 |   25674   30258  1732607    57.3 | 84.318 % |
c |     38785 |   70013   145206 |   28241   30389  1739544    57.2 | 84.328 % |
c |     39010 |   70013   145206 |   31065   30614  1750824    57.2 | 84.328 % |
c |     39349 |   69973   145113 |   34172   30899  1762512    57.0 | 84.436 % |
c |     39855 |   69833   144784 |   37589   31244  1795895    57.5 | 84.529 % |
c |     40614 |   69827   144770 |   41348   32001  1864262    58.3 | 84.535 % |
c |     41754 |   69827   144770 |   45483   33141  1974004    59.6 | 84.535 % |
c |     43462 |   69827   144770 |   50031   34849  2183449    62.7 | 84.535 % |
c |     46024 |   69681   144427 |   55034   37312  2420770    64.9 | 84.698 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48639 |   69628   144300 |   23209   39827  2729728    68.5 | 84.698 % |
c |     48739 |   69610   144258 |   25529   39859  2731474    68.5 | 84.856 % |
c |     48890 |   69610   144258 |   28082   40010  2737338    68.4 | 84.856 % |
c |     49115 |   69610   144258 |   30891   40235  2742174    68.2 | 84.856 % |
c |     49452 |   69610   144258 |   33980   40572  2761799    68.1 | 84.856 % |
c |     49958 |   69598   144230 |   37378   41074  2793086    68.0 | 84.868 % |
c |     50717 |   69598   144230 |   41116   41833  2866027    68.5 | 84.868 % |
c |     51856 |   69598   144230 |   45227   42972  2959760    68.9 | 84.868 % |
c |     53564 |   69598   144230 |   49750   44680  3128717    70.0 | 84.868 % |
c |     56127 |   69598   144230 |   54725   47243  3411584    72.2 | 84.868 % |
c |     59971 |   69592   144216 |   60198   51084  3862493    75.6 | 84.875 % |
c |     65737 |   69574   144174 |   66217   56843  4519242    79.5 | 84.894 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72006 |   69183   143234 |   23061   62248  5115262    82.2 | 84.894 % |
c |     72106 |   69183   143234 |   25367   18910  1353791    71.6 | 85.339 % |
c |     72256 |   69102   143045 |   27903   18987  1359626    71.6 | 85.425 % |
c |     72481 |   69054   142931 |   30694   19176  1370453    71.5 | 85.482 % |
c |     72819 |   69054   142931 |   33763   19514  1393733    71.4 | 85.482 % |
c |     73325 |   68986   142769 |   37139   20013  1441666    72.0 | 85.565 % |
c |     74084 |   68986   142769 |   40853   20772  1504724    72.4 | 85.565 % |
c |     75224 |   68986   142769 |   44939   21912  1614132    73.7 | 85.565 % |
c |     76932 |   68970   142731 |   49433   23615  1774756    75.2 | 85.584 % |
c |     79495 |   68895   142555 |   54376   26158  2005716    76.7 | 85.670 % |
c |     83339 |   68780   142283 |   59814   29987  2452098    81.8 | 85.806 % |
c |     89105 |   68780   142283 |   65795   35753  3230648    90.4 | 85.806 % |
c |     97754 |   68780   142283 |   72375   44402  4156615    93.6 | 85.806 % |
c |    110728 |   68780   142283 |   79612   57376  5424675    94.5 | 85.806 % |
c |    130189 |   68583   141821 |   87574   76785  7474948    97.3 | 86.029 % |
c |    159381 |   68579   141812 |   96331  105976 10687470   100.8 | 86.032 % |
c |    203171 |   68579   141812 |  105964   44127  3580247    81.1 | 86.032 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    251009 |   68619   141910 |   22873   91965  8985323    97.7 | 86.032 % |
c |    251109 |   68619   141910 |   25160   18299  1463324    80.0 | 86.004 % |
c |    251259 |   68494   141615 |   27676   18419  1469563    79.8 | 86.150 % |
c |    251484 |   68490   141606 |   30443   18643  1476588    79.2 | 86.153 % |
c |    251822 |   68490   141606 |   33488   18981  1501642    79.1 | 86.153 % |
c |    252329 |   68480   141583 |   36837   19487  1515069    77.7 | 86.163 % |
c |    253088 |   68480   141583 |   40520   20246  1555411    76.8 | 86.163 % |
c |    254227 |   68480   141583 |   44573   21385  1632098    76.3 | 86.163 % |
c |    255935 |   68480   141583 |   49030   23093  1797296    77.8 | 86.163 % |
c |    258497 |   68376   141342 |   53933   25648  1981953    77.3 | 86.271 % |
c |    262341 |   68356   141296 |   59326   29487  2344725    79.5 | 86.290 % |
c |    268108 |   68340   141258 |   65259   35252  2875389    81.6 | 86.309 % |
c |    276759 |   68264   141078 |   71785   43879  3630273    82.7 | 86.398 % |
c |    289733 |   68264   141078 |   78963   56853  5112104    89.9 | 86.398 % |
c |    309194 |   68264   141078 |   86860   76314  7402587    97.0 | 86.398 % |
c |    338386 |   68264   141078 |   95546  105506 10546661   100.0 | 86.398 % |
c |    382175 |   68234   141008 |  105100   43730  4523969   103.5 | 86.429 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 C508 -C507 -C506 -C505 -C504 C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 C380 -C379 -C378 -C377 -C376 -C375 -C374 C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265#### 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.91 0.95 0.90 2/54 2088
Raw data (stat): 2088 (runsolver) R 2087 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481801646 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99942 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 3806 0 0 0 987 11 0 0 25 0 1 0 481801646 17588224 3784 4294967295 134512640 134672761 3221224560 3221223732 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4294 3784 603 41 0 4253 0
vsize: 17176
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 3813 0 0 0 1986 11 0 0 25 0 1 0 481801646 17588224 3791 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3791 603 41 0 4253 0
vsize: 17176
[startup+30.0005 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 3930 0 0 0 2986 12 0 0 25 0 1 0 481801646 18464768 3908 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4508 3908 603 41 0 4467 0
vsize: 18032
[startup+40.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 3932 0 0 0 3985 12 0 0 25 0 1 0 481801646 18464768 3910 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4508 3910 603 41 0 4467 0
vsize: 18032
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 3932 0 0 0 4985 12 0 0 25 0 1 0 481801646 18464768 3910 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4508 3910 603 41 0 4467 0
vsize: 18032
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 4105 0 0 0 5985 13 0 0 25 0 1 0 481801646 19140608 4083 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4673 4083 603 41 0 4632 0
vsize: 18692
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 4520 0 0 0 6983 14 0 0 25 0 1 0 481801646 20869120 4498 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5095 4498 603 41 0 5054 0
vsize: 20380
[startup+80.0018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 5160 0 0 0 7982 15 0 0 25 0 1 0 481801646 23429120 5138 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5720 5138 603 41 0 5679 0
vsize: 22880
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 5742 0 0 0 8980 18 0 0 25 0 1 0 481801646 25837568 5720 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6308 5720 603 41 0 6267 0
vsize: 25232
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 6293 0 0 0 9978 19 0 0 25 0 1 0 481801646 28237824 6271 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6894 6271 603 41 0 6853 0
vsize: 27576
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 6821 0 0 0 10976 22 0 0 25 0 1 0 481801646 30339072 6799 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7407 6799 603 41 0 7366 0
vsize: 29628
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 7296 0 0 0 11975 23 0 0 25 0 1 0 481801646 32202752 7274 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7862 7274 603 41 0 7821 0
vsize: 31448
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 7831 0 0 0 12974 24 0 0 25 0 1 0 481801646 34484224 7809 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8419 7809 603 41 0 8378 0
vsize: 33676
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 8277 0 0 0 13973 25 0 0 25 0 1 0 481801646 36220928 8255 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8843 8255 603 41 0 8802 0
vsize: 35372
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 8699 0 0 0 14972 26 0 0 25 0 1 0 481801646 37949440 8677 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9265 8677 603 41 0 9224 0
vsize: 37060
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9084 0 0 0 15971 28 0 0 25 0 1 0 481801646 39555072 9062 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9657 9062 603 41 0 9616 0
vsize: 38628
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9406 0 0 0 16970 29 0 0 25 0 1 0 481801646 40800256 9384 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9961 9384 603 41 0 9920 0
vsize: 39844
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9406 0 0 0 17970 29 0 0 25 0 1 0 481801646 40800256 9384 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9961 9384 603 41 0 9920 0
vsize: 39844
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9406 0 0 0 18970 29 0 0 25 0 1 0 481801646 40800256 9384 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9961 9384 603 41 0 9920 0
vsize: 39844
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9406 0 0 0 19970 29 0 0 25 0 1 0 481801646 40800256 9384 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9961 9384 603 41 0 9920 0
vsize: 39844
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9406 0 0 0 20970 29 0 0 25 0 1 0 481801646 40800256 9384 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9961 9384 603 41 0 9920 0
vsize: 39844
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9406 0 0 0 21971 29 0 0 25 0 1 0 481801646 40800256 9384 4294967295 134512640 134672761 3221224560 3221223744 134559569 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9961 9384 603 41 0 9920 0
vsize: 39844
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9406 0 0 0 22971 29 0 0 25 0 1 0 481801646 40800256 9384 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9961 9384 603 41 0 9920 0
vsize: 39844
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9406 0 0 0 23971 29 0 0 25 0 1 0 481801646 40800256 9384 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9961 9384 603 41 0 9920 0
vsize: 39844
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 9767 0 0 0 24970 30 0 0 25 0 1 0 481801646 42258432 9745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10317 9745 603 41 0 10276 0
vsize: 41268
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 10191 0 0 0 25969 31 0 0 25 0 1 0 481801646 44118016 10169 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 10169 603 41 0 10730 0
vsize: 43084
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 10633 0 0 0 26968 33 0 0 25 0 1 0 481801646 45846528 10611 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11193 10611 603 41 0 11152 0
vsize: 44772
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 11023 0 0 0 27966 34 0 0 25 0 1 0 481801646 47706112 11001 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11647 11001 603 41 0 11606 0
vsize: 46588
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 11341 0 0 0 28965 35 0 0 25 0 1 0 481801646 49033216 11319 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11971 11319 603 41 0 11930 0
vsize: 47884
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 11639 0 0 0 29965 36 0 0 25 0 1 0 481801646 50221056 11617 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12261 11617 603 41 0 12220 0
vsize: 49044
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 11936 0 0 0 30964 37 0 0 25 0 1 0 481801646 51408896 11914 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12551 11914 603 41 0 12510 0
vsize: 50204
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 12305 0 0 0 31963 39 0 0 25 0 1 0 481801646 52879360 12283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12910 12283 603 41 0 12869 0
vsize: 51640
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 12639 0 0 0 32962 39 0 0 25 0 1 0 481801646 54333440 12617 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13265 12617 603 41 0 13224 0
vsize: 53060
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 12958 0 0 0 33961 41 0 0 25 0 1 0 481801646 55533568 12936 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13558 12936 603 41 0 13517 0
vsize: 54232
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 13300 0 0 0 34960 42 0 0 25 0 1 0 481801646 57004032 13278 4294967295 134512640 134672761 3221224560 3221223744 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13917 13278 603 41 0 13876 0
vsize: 55668
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 13579 0 0 0 35960 42 0 0 25 0 1 0 481801646 58077184 13557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14179 13557 603 41 0 14138 0
vsize: 56716
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 13843 0 0 0 36959 43 0 0 25 0 1 0 481801646 59138048 13821 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14438 13821 603 41 0 14397 0
vsize: 57752
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 14131 0 0 0 37959 44 0 0 25 0 1 0 481801646 60354560 14109 4294967295 134512640 134672761 3221224560 3221223744 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14735 14109 603 41 0 14694 0
vsize: 58940
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 14430 0 0 0 38958 45 0 0 25 0 1 0 481801646 61546496 14408 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15026 14408 603 41 0 14985 0
vsize: 60104
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 14712 0 0 0 39957 46 0 0 25 0 1 0 481801646 62742528 14690 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15318 14690 603 41 0 15277 0
vsize: 61272
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 14998 0 0 0 40957 46 0 0 25 0 1 0 481801646 63803392 14976 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15577 14976 603 41 0 15536 0
vsize: 62308
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 15258 0 0 0 41956 47 0 0 25 0 1 0 481801646 64864256 15236 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15836 15236 603 41 0 15795 0
vsize: 63344
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 15518 0 0 0 42955 48 0 0 25 0 1 0 481801646 65929216 15496 4294967295 134512640 134672761 3221224560 3221223664 134559760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16096 15496 603 41 0 16055 0
vsize: 64384
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 15747 0 0 0 43953 50 0 0 25 0 1 0 481801646 66859008 15725 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16323 15725 603 41 0 16282 0
vsize: 65292
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 15959 0 0 0 44952 50 0 0 25 0 1 0 481801646 67784704 15937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16549 15937 603 41 0 16508 0
vsize: 66196
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 16192 0 0 0 45952 51 0 0 25 0 1 0 481801646 68718592 16170 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16777 16170 603 41 0 16736 0
vsize: 67108
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 16389 0 0 0 46952 52 0 0 25 0 1 0 481801646 69529600 16367 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16975 16367 603 41 0 16934 0
vsize: 67900
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 16587 0 0 0 47951 53 0 0 25 0 1 0 481801646 70324224 16565 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17169 16565 603 41 0 17128 0
vsize: 68676
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 16752 0 0 0 48951 53 0 0 25 0 1 0 481801646 71016448 16730 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17338 16730 603 41 0 17297 0
vsize: 69352
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 16956 0 0 0 49950 54 0 0 25 0 1 0 481801646 71831552 16934 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17537 16934 603 41 0 17496 0
vsize: 70148
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17114 0 0 0 50950 54 0 0 25 0 1 0 481801646 72511488 17092 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17703 17092 603 41 0 17662 0
vsize: 70812
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17267 0 0 0 51950 55 0 0 25 0 1 0 481801646 73039872 17245 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17832 17245 603 41 0 17791 0
vsize: 71328
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 52949 55 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 53950 55 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 54950 55 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 55950 55 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 56950 55 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 57950 55 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 58950 55 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 59950 55 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 60949 56 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223664 134560207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 61949 56 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17350 0 0 0 62949 57 0 0 25 0 1 0 481801646 73433088 17328 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17328 603 41 0 17887 0
vsize: 71712
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17351 0 0 0 63949 57 0 0 25 0 1 0 481801646 73433088 17329 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17329 603 41 0 17887 0
vsize: 71712
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17351 0 0 0 64949 57 0 0 25 0 1 0 481801646 73433088 17329 4294967295 134512640 134672761 3221224560 3221223744 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17329 603 41 0 17887 0
vsize: 71712
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17351 0 0 0 65948 58 0 0 25 0 1 0 481801646 73433088 17329 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17329 603 41 0 17887 0
vsize: 71712
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 66948 58 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 67948 58 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223664 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 68948 58 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 69948 58 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 70948 58 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 71948 58 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 72949 58 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 73949 58 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223860 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 74949 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 75949 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 76949 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 77949 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 78949 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 79950 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 80950 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 81950 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 82950 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 83950 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 84951 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223664 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 85951 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 86951 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 87951 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 88951 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 89952 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 90952 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 91952 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 92952 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 93952 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+950.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 94953 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223664 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 95953 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2088
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 96953 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223744 134559489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2089
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 97953 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+990.206 s]
Raw data (loadavg): 1.07 0.99 0.91 2/58 2131
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 98971 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1000.21 s]
Raw data (loadavg): 1.22 1.02 0.93 2/54 2141
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 99971 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1010.21 s]
Raw data (loadavg): 1.18 1.02 0.93 2/54 2141
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 100971 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223744 134559559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1020.21 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 2141
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 101971 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1030.21 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 2141
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 102972 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1040.21 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 2141
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 103972 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1050.21 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 2141
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 104972 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1060.21 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 105972 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1070.21 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17353 0 0 0 106972 59 0 0 25 0 1 0 481801646 73433088 17331 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17928 17331 603 41 0 17887 0
vsize: 71712
[startup+1080.21 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17646 0 0 0 107972 60 0 0 25 0 1 0 481801646 74625024 17624 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18219 17624 603 41 0 18178 0
vsize: 72876
[startup+1090.21 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 17930 0 0 0 108971 60 0 0 25 0 1 0 481801646 75821056 17908 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18511 17908 603 41 0 18470 0
vsize: 74044
[startup+1100.21 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18207 0 0 0 109970 61 0 0 25 0 1 0 481801646 76886016 18185 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18771 18185 603 41 0 18730 0
vsize: 75084
[startup+1110.21 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18231 0 0 0 110970 61 0 0 25 0 1 0 481801646 77021184 18209 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18209 603 41 0 18763 0
vsize: 75216
[startup+1120.21 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18231 0 0 0 111971 61 0 0 25 0 1 0 481801646 77021184 18209 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18209 603 41 0 18763 0
vsize: 75216
[startup+1130.21 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18231 0 0 0 112971 61 0 0 25 0 1 0 481801646 77021184 18209 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18209 603 41 0 18763 0
vsize: 75216
[startup+1140.21 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18231 0 0 0 113971 61 0 0 25 0 1 0 481801646 77021184 18209 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18209 603 41 0 18763 0
vsize: 75216
[startup+1150.21 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18231 0 0 0 114971 61 0 0 25 0 1 0 481801646 77021184 18209 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18209 603 41 0 18763 0
vsize: 75216
[startup+1160.21 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18231 0 0 0 115971 61 0 0 25 0 1 0 481801646 77021184 18209 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18209 603 41 0 18763 0
vsize: 75216
[startup+1170.21 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18232 0 0 0 116971 61 0 0 25 0 1 0 481801646 77021184 18210 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18210 603 41 0 18763 0
vsize: 75216
[startup+1180.21 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18232 0 0 0 117971 61 0 0 25 0 1 0 481801646 77021184 18210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18210 603 41 0 18763 0
vsize: 75216
[startup+1190.21 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18232 0 0 0 118971 61 0 0 25 0 1 0 481801646 77021184 18210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18210 603 41 0 18763 0
vsize: 75216
[startup+1200.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2143
Raw data (stat): 2088 (minisat+) R 2087 27222 27221 0 -1 0 18232 0 0 0 119971 61 0 0 25 0 1 0 481801646 77021184 18210 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18804 18210 603 41 0 18763 0
vsize: 75216
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 2143
Raw data (stat): 2088 (minisat+) Z 2087 27222 27221 0 -1 12 18235 0 0 0 119972 65 0 0 25 0 1 0 481801646 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.25
CPU time (s): 1200.37
CPU user time (s): 1199.72
CPU system time (s): 0.6539
CPU usage (%): 100.011
Max. virtual memory (Kb): 75216
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####