PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        876012 kB
Buffers:         36436 kB
Cached:          99572 kB
SwapCached:       2644 kB
Active:          55884 kB
Inactive:        85664 kB
HighTotal:      131008 kB
HighFree:        27580 kB
LowTotal:       903652 kB
LowFree:        848432 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11512 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:17:55 (client local time) WITH STATUS 10 IN 1200.41 SECONDS
stats: 4476 7 1200.41 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94289 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   94289   188578 |   31429       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70300     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  169363   364695 |   56454       0        0     nan |  0.000 % |
c |       100 |  168931   363803 |   62099      75      961    12.8 |  0.464 % |
c |       251 |  168226   362304 |   68309     195     2080    10.7 |  1.241 % |
c |       477 |  166908   359478 |   75140     361     4481    12.4 |  2.716 % |
c |       814 |  165085   355491 |   82654     634     6941    10.9 |  4.833 % |
c |      1320 |  161650   347896 |   90919    1002    11746    11.7 |  8.903 % |
c |      2079 |  157439   338515 |  100011    1501    17642    11.8 | 13.952 % |
c |      3218 |  149574   320611 |  110012    2257    27487    12.2 | 23.762 % |
c |      4926 |  140077   298909 |  121014    3343    40938    12.2 | 35.604 % |
c |      7488 |  129263   273622 |  133115    4970    57038    11.5 | 49.390 % |
c |     11332 |  118074   247204 |  146427    7283    85078    11.7 | 64.089 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14173 |  112053   232947 |   37351    8812   110869    12.6 | 64.089 % |
c |     14273 |  111956   232718 |   41086    8872   112201    12.6 | 72.341 % |
c |     14423 |  111733   232187 |   45194    9002   114113    12.7 | 72.561 % |
c |     14649 |  111451   231507 |   49714    9151   118315    12.9 | 72.945 % |
c |     14986 |  111001   230402 |   54685    9390   121727    13.0 | 73.568 % |
c |     15492 |  110268   228664 |   60154    9746   131154    13.5 | 74.539 % |
c |     16252 |  109470   226728 |   66169   10246   139678    13.6 | 75.632 % |
c |     17391 |  108305   223901 |   72786   11038   156782    14.2 | 77.225 % |
c |     19099 |  106843   220411 |   80065   12116   192204    15.9 | 79.176 % |
c |     21662 |  105578   217316 |   88071   13811   254342    18.4 | 80.914 % |
c |     25506 |  104256   214065 |   96878   16859   438700    26.0 | 82.765 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29128 |  104139   213840 |   34713   20366   654650    32.1 | 82.765 % |
c |     29229 |  104025   213562 |   38184   20446   657035    32.1 | 83.099 % |
c |     29380 |  103872   213177 |   42002   20466   657976    32.1 | 83.323 % |
c |     29605 |  103872   213177 |   46203   20691   675471    32.6 | 83.323 % |
c |     29942 |  103872   213177 |   50823   21028   685274    32.6 | 83.323 % |
c |     30448 |  103722   212801 |   55905   21442   702839    32.8 | 83.539 % |
c |     31207 |  103261   211676 |   61496   21792   727090    33.4 | 84.177 % |
c |     32346 |  103261   211676 |   67645   22931   784028    34.2 | 84.177 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33412 |  103252   211633 |   34417   23944   928774    38.8 | 84.177 % |
c |     33512 |  103242   211609 |   37858   24024   929884    38.7 | 84.207 % |
c |     33663 |  103242   211609 |   41644   24175   937156    38.8 | 84.207 % |
c |     33888 |  103242   211609 |   45809   24400   945982    38.8 | 84.207 % |
c |     34225 |  103106   211272 |   50389   24656   961580    39.0 | 84.396 % |
c |     34731 |  103096   211246 |   55428   25109   984488    39.2 | 84.412 % |
c |     35491 |  103053   211129 |   60971   25751  1012426    39.3 | 84.478 % |
c |     36631 |  102901   210759 |   67068   26726  1066796    39.9 | 84.686 % |
c |     38339 |  102881   210709 |   73775   28397  1192012    42.0 | 84.715 % |
c |     40901 |  102881   210709 |   81153   30959  1469684    47.5 | 84.715 % |
c |     44746 |  102871   210685 |   89268   34788  1844984    53.0 | 84.729 % |
c ==============================================================================
c [1mFound solution: -45[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 |     49083 |  102808   210537 |   34269   39065  2552883    65.3 | 84.729 % |
c |     49183 |  102715   210319 |   37695   39094  2554059    65.3 | 84.952 % |
c |     49333 |  102715   210319 |   41465   39244  2564935    65.4 | 84.952 % |
c |     49559 |  102638   210132 |   45612   39228  2570691    65.5 | 85.059 % |
c |     49896 |  102638   210132 |   50173   39565  2591937    65.5 | 85.059 % |
c |     50403 |  102638   210132 |   55190   40072  2655788    66.3 | 85.059 % |
c |     51162 |  102638   210132 |   60709   40831  2713978    66.5 | 85.059 % |
c |     52301 |  102627   210103 |   66780   41795  2803087    67.1 | 85.076 % |
c |     54009 |  102492   209776 |   73458   43288  3004323    69.4 | 85.263 % |
c |     56573 |  102482   209754 |   80804   45807  3307196    72.2 | 85.275 % |
c |     60417 |  102434   209638 |   88884   49598  3816497    76.9 | 85.341 % |
c |     66183 |  102321   209365 |   97773   54712  4533488    82.9 | 85.496 % |
c |     74832 |  102098   208818 |  107550   62430  5539945    88.7 | 85.806 % |
c |     87807 |  101884   208284 |  118305   75224  8117231   107.9 | 86.117 % |
c ==============================================================================
c [1mFound solution: -46[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 |     89873 |  101873   208219 |   33957   77213  8366826   108.4 | 86.117 % |
c |     89973 |  101813   208079 |   37352   77250  8370963   108.4 | 86.209 % |
c |     90123 |  101813   208079 |   41087   77400  8384920   108.3 | 86.209 % |
c |     90348 |  101813   208079 |   45196   77625  8402830   108.2 | 86.209 % |
c |     90685 |  101813   208079 |   49716   77962  8425118   108.1 | 86.209 % |
c |     91191 |  101808   208066 |   54688   78418  8477500   108.1 | 86.217 % |
c |     91950 |  101769   207969 |   60156   79147  8535292   107.8 | 86.273 % |
c |     93089 |  101732   207878 |   66172   79954  8650341   108.2 | 86.324 % |
c |     94797 |  101691   207781 |   72789   81587  8836109   108.3 | 86.378 % |
c |     97360 |  101678   207750 |   80068   84139  9093070   108.1 | 86.396 % |
c |    101204 |  101587   207532 |   88075   87350  9467343   108.4 | 86.516 % |
c |    106970 |  101584   207525 |   96883   93115 10262644   110.2 | 86.520 % |
c |    115619 |  101584   207525 |  106571  101764 11400274   112.0 | 86.520 % |
c ==============================================================================
c [1mFound solution: -47[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128246 |  101576   207519 |   33858  113993 13276183   116.5 | 86.520 % |
c |    128346 |  101576   207519 |   37243   20346  1966312    96.6 | 86.569 % |
c |    128496 |  101576   207519 |   40968   20496  1972565    96.2 | 86.569 % |
c |    128722 |  101576   207519 |   45064   20722  1990233    96.0 | 86.569 % |
c |    129059 |  101576   207519 |   49571   21059  2010034    95.4 | 86.569 % |
c |    129565 |  101573   207512 |   54528   21564  2043549    94.8 | 86.573 % |
c |    130325 |  101573   207512 |   59981   22324  2119304    94.9 | 86.573 % |
c |    131466 |  101573   207512 |   65979   23465  2227953    94.9 | 86.573 % |
c |    133174 |  101566   207497 |   72577   25171  2440505    97.0 | 86.580 % |
c |    135736 |  101564   207493 |   79835   27732  2748292    99.1 | 86.582 % |
c |    139581 |  101564   207493 |   87818   31577  3280586   103.9 | 86.582 % |
c |    145347 |  101564   207493 |   96600   37343  4140110   110.9 | 86.582 % |
c |    153996 |  101564   207493 |  106260   45992  5223572   113.6 | 86.582 % |
c |    166970 |  101517   207383 |  116886   58757  6847744   116.5 | 86.641 % |
c |    186431 |  101502   207348 |  128575   78195  9333628   119.4 | 86.660 % |
c |    215624 |  101465   207263 |  141433  107203 13487587   125.8 | 86.705 % |
c |    259413 |  101459   207249 |  155576  150988 19357146   128.2 | 86.712 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 #### 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.84 0.94 0.90 2/54 2555
Raw data (stat): 2555 (runsolver) R 2554 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422947198 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.99957 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5637 0 0 0 983 14 0 0 25 0 1 0 422947198 26091520 5615 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6370 5615 603 41 0 6329 0
vsize: 25480
[startup+19.9997 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5647 0 0 0 1983 14 0 0 25 0 1 0 422947198 26091520 5625 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6370 5625 603 41 0 6329 0
vsize: 25480
[startup+29.9999 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5653 0 0 0 2983 15 0 0 25 0 1 0 422947198 26226688 5631 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6403 5631 603 41 0 6362 0
vsize: 25612
[startup+39.9989 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5660 0 0 0 3983 15 0 0 25 0 1 0 422947198 26226688 5638 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6403 5638 603 41 0 6362 0
vsize: 25612
[startup+49.9991 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5667 0 0 0 4983 15 0 0 25 0 1 0 422947198 26226688 5645 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6403 5645 603 41 0 6362 0
vsize: 25612
[startup+59.9986 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5675 0 0 0 5984 15 0 0 25 0 1 0 422947198 26226688 5653 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6403 5653 603 41 0 6362 0
vsize: 25612
[startup+69.9984 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5677 0 0 0 6984 15 0 0 25 0 1 0 422947198 26226688 5655 4294967295 134512640 134672761 3221224560 3221223756 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6403 5655 603 41 0 6362 0
vsize: 25612
[startup+79.9985 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5684 0 0 0 7984 15 0 0 25 0 1 0 422947198 26357760 5662 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5662 603 41 0 6394 0
vsize: 25740
[startup+89.9977 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5698 0 0 0 8985 15 0 0 25 0 1 0 422947198 26357760 5676 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5676 603 41 0 6394 0
vsize: 25740
[startup+99.9969 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5863 0 0 0 9984 15 0 0 25 0 1 0 422947198 27406336 5841 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6691 5841 603 41 0 6650 0
vsize: 26764
[startup+109.997 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5866 0 0 0 10983 16 0 0 25 0 1 0 422947198 27406336 5844 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6691 5844 603 41 0 6650 0
vsize: 26764
[startup+119.997 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 6091 0 0 0 11983 16 0 0 25 0 1 0 422947198 28344320 6069 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6920 6069 603 41 0 6879 0
vsize: 27680
[startup+129.997 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2555
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 6450 0 0 0 12983 17 0 0 25 0 1 0 422947198 29827072 6428 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7282 6428 603 41 0 7241 0
vsize: 29128
[startup+139.996 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2608
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 6830 0 0 0 13981 19 0 0 25 0 1 0 422947198 31379456 6808 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7661 6808 603 41 0 7620 0
vsize: 30644
[startup+149.997 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 2608
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 7399 0 0 0 14979 21 0 0 25 0 1 0 422947198 33669120 7377 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8220 7377 603 41 0 8179 0
vsize: 32880
[startup+159.996 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 2608
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 8001 0 0 0 15978 23 0 0 25 0 1 0 422947198 36343808 7979 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8873 7979 603 41 0 8832 0
vsize: 35492
[startup+169.995 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 2608
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 8627 0 0 0 16977 24 0 0 25 0 1 0 422947198 38817792 8605 4294967295 134512640 134672761 3221224560 3221223576 1075352757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9477 8605 603 41 0 9436 0
vsize: 37908
[startup+179.994 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 2608
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 9069 0 0 0 17975 26 0 0 25 0 1 0 422947198 40697856 9047 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9936 9047 603 41 0 9895 0
vsize: 39744
[startup+189.994 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 2608
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 9646 0 0 0 18973 28 0 0 25 0 1 0 422947198 42979328 9624 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10493 9624 603 41 0 10452 0
vsize: 41972
[startup+199.993 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 2608
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 10037 0 0 0 19972 29 0 0 25 0 1 0 422947198 44589056 10015 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10886 10015 603 41 0 10845 0
vsize: 43544
[startup+209.992 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 10592 0 0 0 20970 31 0 0 25 0 1 0 422947198 46870528 10570 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11443 10570 603 41 0 11402 0
vsize: 45772
[startup+219.993 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 11049 0 0 0 21969 33 0 0 25 0 1 0 422947198 48742400 11027 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11900 11027 603 41 0 11859 0
vsize: 47600
[startup+229.993 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 11418 0 0 0 22968 34 0 0 25 0 1 0 422947198 50204672 11396 4294967295 134512640 134672761 3221224560 3221223664 134555114 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12257 11396 603 41 0 12216 0
vsize: 49028
[startup+239.992 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 11720 0 0 0 23967 35 0 0 25 0 1 0 422947198 51412992 11698 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12552 11698 603 41 0 12511 0
vsize: 50208
[startup+249.992 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 12231 0 0 0 24966 37 0 0 25 0 1 0 422947198 53821440 12209 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13140 12209 603 41 0 13099 0
vsize: 52560
[startup+259.992 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 12777 0 0 0 25965 38 0 0 25 0 1 0 422947198 55967744 12755 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13664 12755 603 41 0 13623 0
vsize: 54656
[startup+269.991 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 13305 0 0 0 26964 39 0 0 25 0 1 0 422947198 58101760 13283 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14185 13283 603 41 0 14144 0
vsize: 56740
[startup+279.991 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 13825 0 0 0 27963 41 0 0 25 0 1 0 422947198 60243968 13803 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14708 13803 603 41 0 14667 0
vsize: 58832
[startup+289.991 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 14326 0 0 0 28961 43 0 0 25 0 1 0 422947198 62251008 14304 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15198 14304 603 41 0 15157 0
vsize: 60792
[startup+299.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 14630 0 0 0 29961 43 0 0 25 0 1 0 422947198 63508480 14608 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15505 14608 603 41 0 15464 0
vsize: 62020
[startup+309.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 14879 0 0 0 30961 44 0 0 25 0 1 0 422947198 64581632 14857 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 14857 603 41 0 15726 0
vsize: 63068
[startup+319.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 15202 0 0 0 31961 44 0 0 25 0 1 0 422947198 65921024 15180 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 15180 603 41 0 16053 0
vsize: 64376
[startup+329.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 15471 0 0 0 32960 45 0 0 25 0 1 0 422947198 66994176 15449 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16356 15449 603 41 0 16315 0
vsize: 65424
[startup+339.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 15737 0 0 0 33960 46 0 0 25 0 1 0 422947198 68067328 15715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16618 15715 603 41 0 16577 0
vsize: 66472
[startup+349.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 16078 0 0 0 34959 47 0 0 25 0 1 0 422947198 69410816 16056 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16946 16056 603 41 0 16905 0
vsize: 67784
[startup+359.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 16405 0 0 0 35958 48 0 0 25 0 1 0 422947198 70750208 16383 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17273 16383 603 41 0 17232 0
vsize: 69092
[startup+369.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 16742 0 0 0 36957 50 0 0 25 0 1 0 422947198 72093696 16720 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17601 16720 603 41 0 17560 0
vsize: 70404
[startup+379.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 17029 0 0 0 37957 50 0 0 25 0 1 0 422947198 73277440 17007 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17890 17007 603 41 0 17849 0
vsize: 71560
[startup+389.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 17327 0 0 0 38956 51 0 0 25 0 1 0 422947198 74469376 17305 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18181 17305 603 41 0 18140 0
vsize: 72724
[startup+399.991 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 17627 0 0 0 39956 52 0 0 25 0 1 0 422947198 75792384 17605 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18504 17605 603 41 0 18463 0
vsize: 74016
[startup+409.99 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 17914 0 0 0 40955 53 0 0 25 0 1 0 422947198 76849152 17892 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18762 17892 603 41 0 18721 0
vsize: 75048
[startup+419.991 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 18190 0 0 0 41955 54 0 0 25 0 1 0 422947198 78049280 18168 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19055 18168 603 41 0 19014 0
vsize: 76220
[startup+429.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 18481 0 0 0 42955 54 0 0 25 0 1 0 422947198 79245312 18459 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19347 18459 603 41 0 19306 0
vsize: 77388
[startup+439.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2610
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 18832 0 0 0 43954 55 0 0 25 0 1 0 422947198 80580608 18810 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19673 18810 603 41 0 19632 0
vsize: 78692
[startup+449.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19207 0 0 0 44953 56 0 0 25 0 1 0 422947198 82178048 19185 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20063 19185 603 41 0 20022 0
vsize: 80252
[startup+459.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19574 0 0 0 45953 57 0 0 25 0 1 0 422947198 83648512 19552 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20422 19552 603 41 0 20381 0
vsize: 81688
[startup+469.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 46953 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+479.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 47953 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+489.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 48953 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+499.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 49954 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+509.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 50954 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+519.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 51954 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+529.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 52955 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+539.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 53955 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+549.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 54955 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+559.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 55956 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+569.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 56956 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+579.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 57956 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+589.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 58957 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+599.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 59957 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+609.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 60958 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+619.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 61958 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+629.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 62958 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+639.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 63959 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+649.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 64959 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+659.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 65959 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+669.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 66960 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+679.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 67960 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+689.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 68960 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+699.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 69961 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+709.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 70961 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+719.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 71961 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+729.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 72962 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+739.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 73962 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+749.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 74962 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20696 19835 603 41 0 20655 0
vsize: 82784
[startup+759.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 20159 0 0 0 75962 58 0 0 25 0 1 0 422947198 86110208 20137 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20137 603 41 0 20982 0
vsize: 84092
[startup+769.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 20481 0 0 0 76961 59 0 0 25 0 1 0 422947198 87306240 20459 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20459 603 41 0 21274 0
vsize: 85260
[startup+779.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 20755 0 0 0 77961 60 0 0 25 0 1 0 422947198 88506368 20733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21608 20733 603 41 0 21567 0
vsize: 86432
[startup+789.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 20997 0 0 0 78960 61 0 0 25 0 1 0 422947198 89436160 20975 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21835 20975 603 41 0 21794 0
vsize: 87340
[startup+799.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 21252 0 0 0 79959 62 0 0 25 0 1 0 422947198 90488832 21230 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22092 21230 603 41 0 22051 0
vsize: 88368
[startup+809.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 21567 0 0 0 80958 63 0 0 25 0 1 0 422947198 91828224 21545 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22419 21545 603 41 0 22378 0
vsize: 89676
[startup+819.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 21851 0 0 0 81958 64 0 0 25 0 1 0 422947198 93032448 21829 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22713 21829 603 41 0 22672 0
vsize: 90852
[startup+829.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 22148 0 0 0 82958 65 0 0 25 0 1 0 422947198 94232576 22126 4294967295 134512640 134672761 3221224560 3221223728 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23006 22126 603 41 0 22965 0
vsize: 92024
[startup+839.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 22419 0 0 0 83958 65 0 0 25 0 1 0 422947198 95297536 22397 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23266 22397 603 41 0 23225 0
vsize: 93064
[startup+849.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 22681 0 0 0 84957 66 0 0 25 0 1 0 422947198 96358400 22659 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23525 22659 603 41 0 23484 0
vsize: 94100
[startup+859.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 22936 0 0 0 85956 67 0 0 25 0 1 0 422947198 97427456 22914 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23786 22914 603 41 0 23745 0
vsize: 95144
[startup+869.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 23244 0 0 0 86956 68 0 0 25 0 1 0 422947198 98639872 23222 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24082 23222 603 41 0 24041 0
vsize: 96328
[startup+879.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 23509 0 0 0 87955 69 0 0 25 0 1 0 422947198 100229120 23487 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24470 23487 603 41 0 24429 0
vsize: 97880
[startup+889.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 23785 0 0 0 88954 70 0 0 25 0 1 0 422947198 101433344 23763 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24764 23763 603 41 0 24723 0
vsize: 99056
[startup+899.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 24044 0 0 0 89953 72 0 0 25 0 1 0 422947198 102367232 24022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24992 24022 603 41 0 24951 0
vsize: 99968
[startup+909.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 24310 0 0 0 90952 73 0 0 25 0 1 0 422947198 103444480 24288 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25255 24288 603 41 0 25214 0
vsize: 101020
[startup+919.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 24565 0 0 0 91952 74 0 0 25 0 1 0 422947198 104505344 24543 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25514 24543 603 41 0 25473 0
vsize: 102056
[startup+929.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 24817 0 0 0 92951 74 0 0 25 0 1 0 422947198 105570304 24795 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25774 24795 603 41 0 25733 0
vsize: 103096
[startup+939.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 25054 0 0 0 93951 75 0 0 25 0 1 0 422947198 106487808 25032 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25998 25032 603 41 0 25957 0
vsize: 103992
[startup+949.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 25301 0 0 0 94950 76 0 0 25 0 1 0 422947198 107552768 25279 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26258 25279 603 41 0 26217 0
vsize: 105032
[startup+959.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 25538 0 0 0 95949 77 0 0 25 0 1 0 422947198 108494848 25516 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26488 25516 603 41 0 26447 0
vsize: 105952
[startup+969.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 25778 0 0 0 96949 78 0 0 25 0 1 0 422947198 109547520 25756 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26745 25756 603 41 0 26704 0
vsize: 106980
[startup+979.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26004 0 0 0 97949 79 0 0 25 0 1 0 422947198 110501888 25982 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26978 25982 603 41 0 26937 0
vsize: 107912
[startup+989.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26216 0 0 0 98949 79 0 0 25 0 1 0 422947198 111296512 26194 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27172 26194 603 41 0 27131 0
vsize: 108688
[startup+999.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26461 0 0 0 99948 80 0 0 25 0 1 0 422947198 112361472 26439 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27432 26439 603 41 0 27391 0
vsize: 109728
[startup+1010 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26705 0 0 0 100947 81 0 0 25 0 1 0 422947198 113299456 26683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27661 26683 603 41 0 27620 0
vsize: 110644
[startup+1020 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26945 0 0 0 101947 81 0 0 25 0 1 0 422947198 114245632 26923 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27892 26923 603 41 0 27851 0
vsize: 111568
[startup+1030 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 27186 0 0 0 102946 82 0 0 25 0 1 0 422947198 115187712 27164 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28122 27164 603 41 0 28081 0
vsize: 112488
[startup+1040 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 27437 0 0 0 103945 84 0 0 25 0 1 0 422947198 116240384 27415 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28379 27415 603 41 0 28338 0
vsize: 113516
[startup+1050 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 27669 0 0 0 104944 85 0 0 25 0 1 0 422947198 117166080 27647 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28605 27647 603 41 0 28564 0
vsize: 114420
[startup+1060 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 27916 0 0 0 105944 86 0 0 25 0 1 0 422947198 118235136 27894 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28866 27894 603 41 0 28825 0
vsize: 115464
[startup+1070 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 28154 0 0 0 106943 87 0 0 25 0 1 0 422947198 119164928 28132 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29093 28132 603 41 0 29052 0
vsize: 116372
[startup+1080 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 28386 0 0 0 107943 87 0 0 25 0 1 0 422947198 120098816 28364 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29321 28364 603 41 0 29280 0
vsize: 117284
[startup+1090 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 28630 0 0 0 108942 88 0 0 25 0 1 0 422947198 121167872 28608 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29582 28608 603 41 0 29541 0
vsize: 118328
[startup+1100 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 28876 0 0 0 109942 89 0 0 25 0 1 0 422947198 122093568 28854 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29808 28854 603 41 0 29767 0
vsize: 119232
[startup+1110 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29104 0 0 0 110941 90 0 0 25 0 1 0 422947198 123027456 29082 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30036 29082 603 41 0 29995 0
vsize: 120144
[startup+1120 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29311 0 0 0 111941 91 0 0 25 0 1 0 422947198 123961344 29289 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30264 29289 603 41 0 30223 0
vsize: 121056
[startup+1130 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29491 0 0 0 112941 91 0 0 25 0 1 0 422947198 124624896 29469 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30426 29469 603 41 0 30385 0
vsize: 121704
[startup+1140 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29657 0 0 0 113940 92 0 0 25 0 1 0 422947198 125296640 29635 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30590 29635 603 41 0 30549 0
vsize: 122360
[startup+1150 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29832 0 0 0 114940 92 0 0 25 0 1 0 422947198 126099456 29810 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30786 29810 603 41 0 30745 0
vsize: 123144
[startup+1160 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30024 0 0 0 115940 93 0 0 25 0 1 0 422947198 126767104 30002 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30949 30002 603 41 0 30908 0
vsize: 123796
[startup+1170 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30203 0 0 0 116940 94 0 0 25 0 1 0 422947198 127569920 30181 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31145 30181 603 41 0 31104 0
vsize: 124580
[startup+1180 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30417 0 0 0 117939 94 0 0 25 0 1 0 422947198 128372736 30395 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31341 30395 603 41 0 31300 0
vsize: 125364
[startup+1190 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30677 0 0 0 118940 94 0 0 25 0 1 0 422947198 129568768 30655 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31633 30655 603 41 0 31592 0
vsize: 126532
[startup+1200 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2612
Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30941 0 0 0 119939 95 0 0 25 0 1 0 422947198 130625536 30919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31891 30919 603 41 0 31850 0
vsize: 127564
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 2612
Raw data (stat): 2555 (minisat+) Z 2554 29653 29652 0 -1 12 30944 0 0 0 119940 101 0 0 25 0 1 0 422947198 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.07
CPU time (s): 1200.41
CPU user time (s): 1199.4
CPU system time (s): 1.01285
CPU usage (%): 100.029
Max. virtual memory (Kb): 127564
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####