PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        870580 kB
Buffers:         35956 kB
Cached:         104656 kB
SwapCached:       3276 kB
Active:          69836 kB
Inactive:        76944 kB
HighTotal:      131008 kB
HighFree:        22372 kB
LowTotal:       903652 kB
LowFree:        848208 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11764 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:19:48 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 4090 7 1200.34 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58624 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   58624   117248 |   17587       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   58624   117248 |   23449       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 2.69859 s)
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  104213   224311 |   31263       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/31178          
c   -- var.elim.:  2000/31178          
c   -- var.elim.:  3000/31178          
c   -- var.elim.:  4000/31178          
c   -- var.elim.:  5000/31178          
c   -- var.elim.:  6000/31178          
c   -- var.elim.:  7000/31178          
c   -- var.elim.:  8000/31178          
c   -- var.elim.:  9000/31178          
c   -- var.elim.:  10000/31178          
c   -- var.elim.:  11000/31178          
c   -- var.elim.:  12000/31178          
c   -- var.elim.:  13000/31178          
c   -- var.elim.:  14000/31178          
c   -- var.elim.:  15000/31178          
c   -- var.elim.:  16000/31178          
c   -- var.elim.:  17000/31178          
c   -- var.elim.:  18000/31178          
c   -- var.elim.:  19000/31178          
c   -- var.elim.:  20000/31178          
c   -- var.elim.:  21000/31178          
c   -- var.elim.:  22000/31178          
c   -- var.elim.:  23000/31178          
c   -- var.elim.:  24000/31178          
c   -- var.elim.:  25000/31178          
c   -- var.elim.:  26000/31178          
c   -- var.elim.:  27000/31178          
c   -- var.elim.:  28000/31178          
c   -- var.elim.:  29000/31178          
c   -- var.elim.:  30000/31178          
c   -- var.elim.:  31000/31178          
c   -- var.elim.:  31178/31178          
c   -- var.elim.:  1000/15827          
c   -- var.elim.:  2000/15827          
c   -- var.elim.:  3000/15827          
c   -- var.elim.:  4000/15827          
c   -- var.elim.:  5000/15827          
c   -- var.elim.:  6000/15827          
c   -- var.elim.:  7000/15827          
c   -- var.elim.:  8000/15827          
c   -- var.elim.:  9000/15827          
c   -- var.elim.:  10000/15827          
c   -- var.elim.:  11000/15827          
c   -- var.elim.:  12000/15827          
c   -- var.elim.:  13000/15827          
c   -- var.elim.:  14000/15827          
c   -- var.elim.:  15000/15827          
c   -- var.elim.:  15827/15827          
c   -- var.elim.:  1000/3687          
c   -- var.elim.:  2000/3687          
c   -- var.elim.:  3000/3687          
c   -- var.elim.:  3687/3687          
c   -- subsuming                       
c   -- var.elim.:  1000/7155          
c   -- var.elim.:  2000/7155          
c   -- var.elim.:  3000/7155          
c   -- var.elim.:  4000/7155          
c   -- var.elim.:  5000/7155          
c   -- var.elim.:  6000/7155          
c   -- var.elim.:  7000/7155          
c   -- var.elim.:  7155/7155          
c   -- var.elim.:  661/661          
c   -- subsuming                       
c   -- var.elim.:  452/452          
c   -- var.elim.:  447/447          
c |         0 |   71895   225676 |      --       0       --      -- |     --   | -32318/1366
c |         0 |   71895   225676 |   28758       0        0     nan |  0.000 % |
c |       100 |   71895   225676 |   31633     100    16229   162.3 | 53.135 % |
c |       250 |   71895   225676 |   34797     250    36736   146.9 | 53.135 % |
c |       475 |   71895   225676 |   38276     475    75337   158.6 | 53.135 % |
c |       812 |   71895   225676 |   42104     812   130193   160.3 | 53.135 % |
c |      1318 |   71855   225317 |   46289    1314   249225   189.7 | 53.262 % |
c |      2077 |   71855   225317 |   50918    2073   404264   195.0 | 53.261 % |
c ==============================================================================
c (current CPU-time: 87.2937 s)
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2574 |   76584   238330 |   22975    2570   502736   195.6 | 53.261 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10983          
c   -- var.elim.:  2000/10983          
c   -- var.elim.:  3000/10983          
c   -- var.elim.:  4000/10983          
c   -- var.elim.:  5000/10983          
c   -- var.elim.:  6000/10983          
c   -- var.elim.:  7000/10983          
c   -- var.elim.:  8000/10983          
c   -- var.elim.:  9000/10983          
c   -- var.elim.:  10000/10983          
c   -- var.elim.:  10983/10983          
c   -- var.elim.:  1000/3665          
c   -- var.elim.:  2000/3665          
c   -- var.elim.:  3000/3665          
c   -- var.elim.:  3665/3665          
c |      2574 |   71904   234811 |      --    2570       --      -- |     --   | -4669/1636
c |      2574 |   71904   234811 |   28761    2316   231523   100.0 | 53.261 % |
c |      2674 |   71904   234811 |   31637    2416   243852   100.9 | 60.308 % |
c |      2824 |   71904   234811 |   34801    2566   289521   112.8 | 60.308 % |
c |      3049 |   71904   234811 |   38281    2791   339977   121.8 | 60.308 % |
c |      3386 |   71904   234811 |   42109    3128   386834   123.7 | 60.308 % |
c |      3892 |   71870   234424 |   46298    3631   489198   134.7 | 60.394 % |
c |      4653 |   71870   234424 |   50928    4392   639584   145.6 | 60.394 % |
c |      5792 |   71852   234256 |   56007    5529   935491   169.2 | 60.443 % |
c |      7501 |   71794   233621 |   61558    7230  1345611   186.1 | 60.599 % |
c ==============================================================================
c (current CPU-time: 117.96 s)
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9212 |   80234   255586 |   24070    8921  1723525   193.2 | 60.599 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15409          
c   -- var.elim.:  2000/15409          
c   -- var.elim.:  3000/15409          
c   -- var.elim.:  4000/15409          
c   -- var.elim.:  5000/15409          
c   -- var.elim.:  6000/15409          
c   -- var.elim.:  7000/15409          
c   -- var.elim.:  8000/15409          
c   -- var.elim.:  9000/15409          
c   -- var.elim.:  10000/15409          
c   -- var.elim.:  11000/15409          
c   -- var.elim.:  12000/15409          
c   -- var.elim.:  13000/15409          
c   -- var.elim.:  14000/15409          
c   -- var.elim.:  15000/15409          
c   -- var.elim.:  15409/15409          
c   -- var.elim.:  1000/6234          
c   -- var.elim.:  2000/6234          
c   -- var.elim.:  3000/6234          
c   -- var.elim.:  4000/6234          
c   -- var.elim.:  5000/6234          
c   -- var.elim.:  6000/6234          
c   -- var.elim.:  6234/6234          
c   -- var.elim.:  71/71          
c   -- subsuming                       
c   -- var.elim.:  1000/5294          
c   -- var.elim.:  2000/5294          
c   -- var.elim.:  3000/5294          
c   -- var.elim.:  4000/5294          
c   -- var.elim.:  5000/5294          
c   -- var.elim.:  5294/5294          
c   -- var.elim.:  863/863          
c |      9212 |   71765   239023 |      --    8921       --      -- |     --   | -8445/-15218
c |      9212 |   71765   239023 |   28706    8536  1448686   169.7 | 60.599 % |
c |      9313 |   71765   239023 |   31576    8637  1469632   170.2 | 63.680 % |
c |      9464 |   71765   239023 |   34734    8788  1501179   170.8 | 63.679 % |
c |      9689 |   71765   239023 |   38207    9013  1534872   170.3 | 63.679 % |
c |     10026 |   71765   239023 |   42028    9350  1602630   171.4 | 63.680 % |
c |     10532 |   71654   237890 |   46159    9843  1715641   174.3 | 63.939 % |
c |     11292 |   71618   237536 |   50750   10595  1880974   177.5 | 64.018 % |
c |     12431 |   71618   237536 |   55825   11734  2140814   182.4 | 64.018 % |
c |     14139 |   71365   235041 |   61190   13413  2577833   192.2 | 64.611 % |
c |     16701 |   71197   233486 |   67151   15952  3241896   203.2 | 64.981 % |
c |     20545 |   71055   232066 |   73719   19769  4173240   211.1 | 65.334 % |
c |     26312 |   70747   229024 |   80739   25489  5922736   232.4 | 66.102 % |
c |     34961 |   70577   227239 |   88600   34088  8905832   261.3 | 66.525 % |
c |     47935 |   70035   221985 |   96711   46905 13445394   286.7 | 67.876 % |
c |     67396 |   69653   218274 |  105802   66276 20768467   313.4 | 68.818 % |
c |     96590 |   68892   211009 |  115111   95104 32333910   340.0 | 70.657 % |
c ==============================================================================
c (current CPU-time: 1034.45 s)
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    130290 |   69532   206968 |   20859  128416 46215660   359.9 | 70.657 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6898          
c   -- var.elim.:  2000/6898          
c   -- var.elim.:  3000/6898          
c   -- var.elim.:  4000/6898          
c   -- var.elim.:  5000/6898          
c   -- var.elim.:  6000/6898          
c   -- var.elim.:  6898/6898          
c   -- var.elim.:  997/997          
c |    130290 |   68081   203073 |      --  128416       --      -- |     --   | -1451/-3894
c |    130290 |   68081   203073 |   27232  128211 46117465   359.7 | 70.657 % |
c |    130392 |   68081   203073 |   29955   25530  6108147   239.3 | 73.019 % |
c |    130542 |   68081   203073 |   32951   25680  6161595   239.9 | 73.019 % |
c |    130767 |   68081   203073 |   36246   25905  6218625   240.1 | 73.019 % |
c |    131104 |   68081   203073 |   39870   26242  6357910   242.3 | 73.019 % |
c |    131610 |   68081   203073 |   43858   26748  6496352   242.9 | 73.019 % |
c |    132369 |   68081   203073 |   48243   27507  6729551   244.6 | 73.019 % |
c |    133508 |   68081   203073 |   53068   28646  7155414   249.8 | 73.019 % |
c |    135216 |   68079   203051 |   58373   30351  7739972   255.0 | 73.024 % |
c |    137779 |   68079   203051 |   64210   32914  8660064   263.1 | 73.024 % |
c |    141623 |   68047   202735 |   70598   36753  9921294   269.9 | 73.103 % |
c |    147391 |   67962   201949 |   77561   42510 11842108   278.6 | 73.309 % |
c |    156040 |   67814   200543 |   85131   51133 14821836   289.9 | 73.664 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559#### 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 18323
Raw data (stat): 18323 (runsolver) R 18322 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422235086 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 18323
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 6462 0 0 0 972 27 0 0 25 0 1 0 422235086 26705920 6048 4294967295 134512640 134672761 3221224560 3221222992 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6520 6048 603 41 0 6479 0
vsize: 26080
[startup+20.0037 s]
Raw data (loadavg): 0.89 0.94 0.90 4/58 18352
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 6478 0 0 0 1972 27 0 0 25 0 1 0 422235086 26869760 6064 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6560 6064 603 41 0 6519 0
vsize: 26240
[startup+30.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18376
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 6481 0 0 0 2971 27 0 0 25 0 1 0 422235086 26869760 6067 4294967295 134512640 134672761 3221224560 3221222992 134605852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6560 6067 603 41 0 6519 0
vsize: 26240
[startup+40.0057 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18376
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 6510 0 0 0 3971 28 0 0 25 0 1 0 422235086 26869760 6096 4294967295 134512640 134672761 3221224560 3221222432 134566721 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6560 6096 603 41 0 6519 0
vsize: 26240
[startup+50.0065 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18376
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 6519 0 0 0 4971 28 0 0 25 0 1 0 422235086 26869760 6105 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6560 6105 603 41 0 6519 0
vsize: 26240
[startup+60.0069 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18376
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 6520 0 0 0 5971 28 0 0 25 0 1 0 422235086 26869760 6106 4294967295 134512640 134672761 3221224560 3221223008 134643521 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6560 6106 603 41 0 6519 0
vsize: 26240
[startup+70.0072 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18376
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 6724 0 0 0 6970 29 0 0 25 0 1 0 422235086 27852800 6310 4294967295 134512640 134672761 3221224560 3221223120 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6800 6310 603 41 0 6759 0
vsize: 27200
[startup+80.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18376
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 6724 0 0 0 7970 29 0 0 25 0 1 0 422235086 26869760 6106 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6560 6106 603 41 0 6519 0
vsize: 26240
[startup+90.0088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18376
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 8530 0 0 0 8957 42 0 0 25 0 1 0 422235086 32059392 6985 4294967295 134512640 134672761 3221224560 3221222736 134621242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7827 6985 603 41 0 7786 0
vsize: 31308
[startup+100.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 8530 0 0 0 9952 48 0 0 25 0 1 0 422235086 32059392 6985 4294967295 134512640 134672761 3221224560 3221223008 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7827 6985 603 41 0 7786 0
vsize: 31308
[startup+110.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 8778 0 0 0 10951 50 0 0 25 0 1 0 422235086 33189888 7233 4294967295 134512640 134672761 3221224560 3221223664 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7233 603 41 0 8062 0
vsize: 32412
[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 11171 0 0 0 11941 60 0 0 25 0 1 0 422235086 38170624 8447 4294967295 134512640 134672761 3221224560 3221223104 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9319 8447 603 41 0 9278 0
vsize: 37276
[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 11221 0 0 0 12920 81 0 0 25 0 1 0 422235086 36626432 8233 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8233 603 41 0 8901 0
vsize: 35768
[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 11221 0 0 0 13920 81 0 0 25 0 1 0 422235086 36626432 8233 4294967295 134512640 134672761 3221224560 3221223008 134643567 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8233 603 41 0 8901 0
vsize: 35768
[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 11425 0 0 0 14919 82 0 0 25 0 1 0 422235086 37806080 8437 4294967295 134512640 134672761 3221224560 3221223088 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9230 8437 603 41 0 9189 0
vsize: 36920
[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 11425 0 0 0 15919 83 0 0 25 0 1 0 422235086 36626432 8233 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8233 603 41 0 8901 0
vsize: 35768
[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 11788 0 0 0 16918 84 0 0 25 0 1 0 422235086 38166528 8596 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9318 8596 603 41 0 9277 0
vsize: 37272
[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 12557 0 0 0 17917 85 0 0 25 0 1 0 422235086 41308160 9365 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10085 9365 603 41 0 10044 0
vsize: 40340
[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 13546 0 0 0 18915 87 0 0 25 0 1 0 422235086 45514752 10354 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11112 10354 603 41 0 11071 0
vsize: 44448
[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 14289 0 0 0 19914 89 0 0 25 0 1 0 422235086 48517120 11097 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11845 11097 603 41 0 11804 0
vsize: 47380
[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 15084 0 0 0 20911 92 0 0 25 0 1 0 422235086 51793920 11892 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12645 11892 603 41 0 12604 0
vsize: 50580
[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 16033 0 0 0 21909 94 0 0 25 0 1 0 422235086 55640064 12841 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13584 12841 603 41 0 13543 0
vsize: 54336
[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 16836 0 0 0 22907 96 0 0 25 0 1 0 422235086 58863616 13644 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14371 13644 603 41 0 14330 0
vsize: 57484
[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 17829 0 0 0 23905 98 0 0 25 0 1 0 422235086 62980096 14637 4294967295 134512640 134672761 3221224560 3221223408 134605852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15376 14637 603 41 0 15335 0
vsize: 61504
[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 18693 0 0 0 24903 101 0 0 25 0 1 0 422235086 66584576 15501 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16256 15501 603 41 0 16215 0
vsize: 65024
[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 19440 0 0 0 25901 103 0 0 25 0 1 0 422235086 69709824 16248 4294967295 134512640 134672761 3221224560 3221223472 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17019 16248 603 41 0 16978 0
vsize: 68076
[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 20159 0 0 0 26899 105 0 0 25 0 1 0 422235086 72626176 16967 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 16967 603 41 0 17690 0
vsize: 70924
[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 20771 0 0 0 27898 107 0 0 25 0 1 0 422235086 75116544 17579 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18339 17579 603 41 0 18298 0
vsize: 73356
[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 21439 0 0 0 28897 108 0 0 25 0 1 0 422235086 77819904 18247 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18999 18247 603 41 0 18958 0
vsize: 75996
[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 21983 0 0 0 29895 109 0 0 25 0 1 0 422235086 80044032 18791 4294967295 134512640 134672761 3221224560 3221223600 134612867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19542 18791 603 41 0 19501 0
vsize: 78168
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 22526 0 0 0 30894 111 0 0 25 0 1 0 422235086 82235392 19334 4294967295 134512640 134672761 3221224560 3221223704 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20077 19334 603 41 0 20036 0
vsize: 80308
[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18378
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 23243 0 0 0 31892 113 0 0 25 0 1 0 422235086 85192704 20051 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20799 20051 603 41 0 20758 0
vsize: 83196
[startup+330.026 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 23881 0 0 0 32890 115 0 0 25 0 1 0 422235086 87818240 20689 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21440 20689 603 41 0 21399 0
vsize: 85760
[startup+340.027 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 24692 0 0 0 33887 118 0 0 25 0 1 0 422235086 91181056 21500 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22261 21500 603 41 0 22220 0
vsize: 89044
[startup+350.028 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 25508 0 0 0 34886 120 0 0 25 0 1 0 422235086 94425088 22316 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23053 22316 603 41 0 23012 0
vsize: 92212
[startup+360.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 25830 0 0 0 35885 121 0 0 25 0 1 0 422235086 95727616 22638 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23371 22638 603 41 0 23330 0
vsize: 93484
[startup+370.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 26534 0 0 0 36884 122 0 0 25 0 1 0 422235086 98705408 23342 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24098 23342 603 41 0 24057 0
vsize: 96392
[startup+380.028 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 26964 0 0 0 37882 124 0 0 25 0 1 0 422235086 100409344 23772 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24514 23772 603 41 0 24473 0
vsize: 98056
[startup+390.029 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 27533 0 0 0 38881 125 0 0 25 0 1 0 422235086 102748160 24341 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25085 24341 603 41 0 25044 0
vsize: 100340
[startup+400.029 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 28082 0 0 0 39880 127 0 0 25 0 1 0 422235086 104951808 24890 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25623 24890 603 41 0 25582 0
vsize: 102492
[startup+410.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 28910 0 0 0 40878 129 0 0 25 0 1 0 422235086 108367872 25718 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26457 25718 603 41 0 26416 0
vsize: 105828
[startup+420.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 29328 0 0 0 41877 131 0 0 25 0 1 0 422235086 110063616 26136 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26871 26137 603 41 0 26830 0
vsize: 107484
[startup+430.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 30080 0 0 0 42875 132 0 0 25 0 1 0 422235086 113106944 26888 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27614 26888 603 41 0 27573 0
vsize: 110456
[startup+440.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 30522 0 0 0 43874 133 0 0 25 0 1 0 422235086 114954240 27330 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28065 27330 603 41 0 28024 0
vsize: 112260
[startup+450.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 31106 0 0 0 44873 135 0 0 25 0 1 0 422235086 117551104 27914 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27914 603 41 0 28658 0
vsize: 114796
[startup+460.032 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 31619 0 0 0 45872 136 0 0 25 0 1 0 422235086 119644160 28427 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29210 28427 603 41 0 29169 0
vsize: 116840
[startup+470.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 32386 0 0 0 46871 138 0 0 25 0 1 0 422235086 122863616 29194 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29996 29194 603 41 0 29955 0
vsize: 119984
[startup+480.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 32977 0 0 0 47868 140 0 0 25 0 1 0 422235086 125214720 29785 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30570 29785 603 41 0 30529 0
vsize: 122280
[startup+490.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 33455 0 0 0 48867 142 0 0 25 0 1 0 422235086 127254528 30263 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31068 30263 603 41 0 31027 0
vsize: 124272
[startup+500.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 33705 0 0 0 49866 142 0 0 25 0 1 0 422235086 128159744 30513 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31289 30513 603 41 0 31248 0
vsize: 125156
[startup+510.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 34382 0 0 0 50865 144 0 0 25 0 1 0 422235086 131002368 31190 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31983 31190 603 41 0 31942 0
vsize: 127932
[startup+520.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 34608 0 0 0 51864 145 0 0 25 0 1 0 422235086 131923968 31416 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32208 31416 603 41 0 32167 0
vsize: 128832
[startup+530.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 35204 0 0 0 52863 146 0 0 25 0 1 0 422235086 134365184 32012 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32804 32012 603 41 0 32763 0
vsize: 131216
[startup+540.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 35788 0 0 0 53862 148 0 0 25 0 1 0 422235086 136708096 32596 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33376 32596 603 41 0 33335 0
vsize: 133504
[startup+550.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 36278 0 0 0 54861 149 0 0 25 0 1 0 422235086 138784768 33086 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33883 33086 603 41 0 33842 0
vsize: 135532
[startup+560.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 36836 0 0 0 55860 150 0 0 25 0 1 0 422235086 140959744 33644 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34414 33644 603 41 0 34373 0
vsize: 137656
[startup+570.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 37168 0 0 0 56859 152 0 0 25 0 1 0 422235086 142405632 33976 4294967295 134512640 134672761 3221224560 3221223744 134615773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34767 33976 603 41 0 34726 0
vsize: 139068
[startup+580.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 37895 0 0 0 57858 153 0 0 25 0 1 0 422235086 145383424 34703 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35494 34703 603 41 0 35453 0
vsize: 141976
[startup+590.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 38469 0 0 0 58856 155 0 0 25 0 1 0 422235086 147742720 35277 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36070 35277 603 41 0 36029 0
vsize: 144280
[startup+600.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 38949 0 0 0 59854 157 0 0 25 0 1 0 422235086 149708800 35757 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36550 35757 603 41 0 36509 0
vsize: 146200
[startup+610.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 39343 0 0 0 60854 157 0 0 25 0 1 0 422235086 151265280 36151 4294967295 134512640 134672761 3221224560 3221223728 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36930 36151 603 41 0 36889 0
vsize: 147720
[startup+620.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 39990 0 0 0 61852 159 0 0 25 0 1 0 422235086 153939968 36798 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37583 36798 603 41 0 37542 0
vsize: 150332
[startup+630.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 40362 0 0 0 62852 159 0 0 25 0 1 0 422235086 155361280 37170 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37930 37170 603 41 0 37889 0
vsize: 151720
[startup+640.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 40908 0 0 0 63851 161 0 0 25 0 1 0 422235086 157708288 37716 4294967295 134512640 134672761 3221224560 3221223704 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38503 37716 603 41 0 38462 0
vsize: 154012
[startup+650.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 41201 0 0 0 64850 162 0 0 25 0 1 0 422235086 158879744 38009 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38789 38009 603 41 0 38748 0
vsize: 155156
[startup+660.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 41394 0 0 0 65850 162 0 0 25 0 1 0 422235086 159666176 38202 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38981 38202 603 41 0 38940 0
vsize: 155924
[startup+670.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 42007 0 0 0 66848 164 0 0 25 0 1 0 422235086 162119680 38815 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39580 38815 603 41 0 39539 0
vsize: 158320
[startup+680.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 42636 0 0 0 67845 165 0 0 25 0 1 0 422235086 164704256 39444 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40211 39444 603 41 0 40170 0
vsize: 160844
[startup+690.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 43022 0 0 0 68845 166 0 0 25 0 1 0 422235086 166240256 39830 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40586 39830 603 41 0 40545 0
vsize: 162344
[startup+700.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 43265 0 0 0 69844 166 0 0 25 0 1 0 422235086 167305216 40073 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40846 40073 603 41 0 40805 0
vsize: 163384
[startup+710.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 43695 0 0 0 70844 167 0 0 25 0 1 0 422235086 169099264 40503 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41284 40503 603 41 0 41243 0
vsize: 165136
[startup+720.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 43972 0 0 0 71843 168 0 0 25 0 1 0 422235086 170156032 40780 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41542 40780 603 41 0 41501 0
vsize: 166168
[startup+730.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 44338 0 0 0 72843 169 0 0 25 0 1 0 422235086 171696128 41146 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41918 41146 603 41 0 41877 0
vsize: 167672
[startup+740.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 45031 0 0 0 73840 172 0 0 25 0 1 0 422235086 174522368 41839 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42608 41839 603 41 0 42567 0
vsize: 170432
[startup+750.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 45545 0 0 0 74839 173 0 0 25 0 1 0 422235086 176615424 42353 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43119 42353 603 41 0 43078 0
vsize: 172476
[startup+760.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 45883 0 0 0 75839 174 0 0 25 0 1 0 422235086 177938432 42691 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43442 42691 603 41 0 43401 0
vsize: 173768
[startup+770.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 46113 0 0 0 76838 174 0 0 25 0 1 0 422235086 178978816 42921 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43696 42921 603 41 0 43655 0
vsize: 174784
[startup+780.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 46328 0 0 0 77838 175 0 0 25 0 1 0 422235086 179781632 43136 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43892 43136 603 41 0 43851 0
vsize: 175568
[startup+790.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 46559 0 0 0 78837 176 0 0 25 0 1 0 422235086 180830208 43367 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44148 43367 603 41 0 44107 0
vsize: 176592
[startup+800.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 46927 0 0 0 79836 177 0 0 25 0 1 0 422235086 182267904 43735 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 43735 603 41 0 44458 0
vsize: 177996
[startup+810.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 47143 0 0 0 80836 177 0 0 25 0 1 0 422235086 183185408 43951 4294967295 134512640 134672761 3221224560 3221223600 134603490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44723 43951 603 41 0 44682 0
vsize: 178892
[startup+820.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 47693 0 0 0 81835 178 0 0 25 0 1 0 422235086 185409536 44501 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45266 44501 603 41 0 45225 0
vsize: 181064
[startup+830.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 48246 0 0 0 82835 179 0 0 25 0 1 0 422235086 187731968 45054 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45833 45054 603 41 0 45792 0
vsize: 183332
[startup+840.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 48750 0 0 0 83833 181 0 0 25 0 1 0 422235086 189698048 45558 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46313 45558 603 41 0 46272 0
vsize: 185252
[startup+850.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 49080 0 0 0 84832 182 0 0 25 0 1 0 422235086 191127552 45888 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46662 45888 603 41 0 46621 0
vsize: 186648
[startup+860.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 49795 0 0 0 85830 184 0 0 25 0 1 0 422235086 193994752 46603 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47362 46603 603 41 0 47321 0
vsize: 189448
[startup+870.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 50376 0 0 0 86829 186 0 0 25 0 1 0 422235086 196341760 47184 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47935 47184 603 41 0 47894 0
vsize: 191740
[startup+880.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 50834 0 0 0 87828 187 0 0 25 0 1 0 422235086 198283264 47642 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48409 47642 603 41 0 48368 0
vsize: 193636
[startup+890.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 50996 0 0 0 88827 187 0 0 25 0 1 0 422235086 198934528 47804 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48568 47804 603 41 0 48527 0
vsize: 194272
[startup+900.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 51279 0 0 0 89827 188 0 0 25 0 1 0 422235086 200110080 48087 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48855 48087 603 41 0 48814 0
vsize: 195420
[startup+910.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 51835 0 0 0 90826 189 0 0 25 0 1 0 422235086 202317824 48643 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49394 48643 603 41 0 49353 0
vsize: 197576
[startup+920.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 52431 0 0 0 91825 190 0 0 25 0 1 0 422235086 204804096 49239 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50001 49239 603 41 0 49960 0
vsize: 200004
[startup+930.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 52793 0 0 0 92825 191 0 0 25 0 1 0 422235086 206258176 49601 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50356 49601 603 41 0 50315 0
vsize: 201424
[startup+940.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 53264 0 0 0 93823 192 0 0 25 0 1 0 422235086 208224256 50072 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50836 50072 603 41 0 50795 0
vsize: 203344
[startup+950.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 53744 0 0 0 94822 194 0 0 25 0 1 0 422235086 210198528 50552 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51318 50552 603 41 0 51277 0
vsize: 205272
[startup+960.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 53989 0 0 0 95822 194 0 0 25 0 1 0 422235086 211247104 50797 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51574 50797 603 41 0 51533 0
vsize: 206296
[startup+970.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 54758 0 0 0 96821 196 0 0 25 0 1 0 422235086 214310912 51566 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52322 51566 603 41 0 52281 0
vsize: 209288
[startup+980.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 55090 0 0 0 97820 196 0 0 25 0 1 0 422235086 215724032 51898 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52667 51898 603 41 0 52626 0
vsize: 210668
[startup+990.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 55540 0 0 0 98820 197 0 0 25 0 1 0 422235086 217518080 52348 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53105 52348 603 41 0 53064 0
vsize: 212420
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 55782 0 0 0 99819 197 0 0 25 0 1 0 422235086 218550272 52590 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53357 52590 603 41 0 53316 0
vsize: 213428
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 56252 0 0 0 100819 198 0 0 25 0 1 0 422235086 220389376 53060 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53806 53060 603 41 0 53765 0
vsize: 215224
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 56701 0 0 0 101818 199 0 0 25 0 1 0 422235086 222347264 53509 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54284 53509 603 41 0 54243 0
vsize: 217136
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 57134 0 0 0 102818 200 0 0 25 0 1 0 422235086 224047104 53942 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54699 53942 603 41 0 54658 0
vsize: 218796
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59442 0 0 0 103803 215 0 0 25 0 1 0 422235086 226942976 54503 4294967295 134512640 134672761 3221224560 3221223104 134621122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55406 54503 603 41 0 55365 0
vsize: 221624
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59442 0 0 0 104799 218 0 0 25 0 1 0 422235086 225345536 54299 4294967295 134512640 134672761 3221224560 3221223816 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55016 54299 603 41 0 54975 0
vsize: 220064
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 105799 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223372 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 106799 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 107799 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 108799 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 109799 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 110800 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 111800 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 112800 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 113800 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 114800 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 115801 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223600 134612873 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 116801 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 117801 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 118801 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18380
Raw data (stat): 18323 (minisat+) R 18322 10720 10719 0 -1 0 59669 0 0 0 119801 219 0 0 25 0 1 0 422235086 225869824 54400 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55144 54400 603 41 0 55103 0
vsize: 220576
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 18380
Raw data (stat): 18323 (minisat+) Z 18322 10720 10719 0 -1 12 59670 0 0 0 119802 231 0 0 25 0 1 0 422235086 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.2
CPU time (s): 1200.34
CPU user time (s): 1198.02
CPU system time (s): 2.31665
CPU usage (%): 100.012
Max. virtual memory (Kb): 221624
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####