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/frb50-23-opb/normalized-frb50-23-1.opb
MD5SUM	ed1ca962177baf0f135b785abad8adea
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-37
Optimality of the best value was proved	NO
Number of terms in the objective function	1150
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	1150
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1150
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	1150
Total number of constraints	80072
Number of constraints which are clauses	80072
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 5628

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        886516 kB
Buffers:         35284 kB
Cached:          75552 kB
SwapCached:          4 kB
Active:          54172 kB
Inactive:        60476 kB
HighTotal:      131008 kB
HighFree:        50876 kB
LowTotal:       903652 kB
LowFree:        835640 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27900 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:22:19 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 4094 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80072 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 |   80072   160144 |   24021       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   80072   160144 |   32028       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.30335 s)
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  147988   319466 |   44396       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/46228          
c   -- var.elim.:  2000/46228          
c   -- var.elim.:  3000/46228          
c   -- var.elim.:  4000/46228          
c   -- var.elim.:  5000/46228          
c   -- var.elim.:  6000/46228          
c   -- var.elim.:  7000/46228          
c   -- var.elim.:  8000/46228          
c   -- var.elim.:  9000/46228          
c   -- var.elim.:  10000/46228          
c   -- var.elim.:  11000/46228          
c   -- var.elim.:  12000/46228          
c   -- var.elim.:  13000/46228          
c   -- var.elim.:  14000/46228          
c   -- var.elim.:  15000/46228          
c   -- var.elim.:  16000/46228          
c   -- var.elim.:  17000/46228          
c   -- var.elim.:  18000/46228          
c   -- var.elim.:  19000/46228          
c   -- var.elim.:  20000/46228          
c   -- var.elim.:  21000/46228          
c   -- var.elim.:  22000/46228          
c   -- var.elim.:  23000/46228          
c   -- var.elim.:  24000/46228          
c   -- var.elim.:  25000/46228          
c   -- var.elim.:  26000/46228          
c   -- var.elim.:  27000/46228          
c   -- var.elim.:  28000/46228          
c   -- var.elim.:  29000/46228          
c   -- var.elim.:  30000/46228          
c   -- var.elim.:  31000/46228          
c   -- var.elim.:  32000/46228          
c   -- var.elim.:  33000/46228          
c   -- var.elim.:  34000/46228          
c   -- var.elim.:  35000/46228          
c   -- var.elim.:  36000/46228          
c   -- var.elim.:  37000/46228          
c   -- var.elim.:  38000/46228          
c   -- var.elim.:  39000/46228          
c   -- var.elim.:  40000/46228          
c   -- var.elim.:  41000/46228          
c   -- var.elim.:  42000/46228          
c   -- var.elim.:  43000/46228          
c   -- var.elim.:  44000/46228          
c   -- var.elim.:  45000/46228          
c   -- var.elim.:  46000/46228          
c   -- var.elim.:  46228/46228          
c   -- var.elim.:  1000/23434          
c   -- var.elim.:  2000/23434          
c   -- var.elim.:  3000/23434          
c   -- var.elim.:  4000/23434          
c   -- var.elim.:  5000/23434          
c   -- var.elim.:  6000/23434          
c   -- var.elim.:  7000/23434          
c   -- var.elim.:  8000/23434          
c   -- var.elim.:  9000/23434          
c   -- var.elim.:  10000/23434          
c   -- var.elim.:  11000/23434          
c   -- var.elim.:  12000/23434          
c   -- var.elim.:  13000/23434          
c   -- var.elim.:  14000/23434          
c   -- var.elim.:  15000/23434          
c   -- var.elim.:  16000/23434          
c   -- var.elim.:  17000/23434          
c   -- var.elim.:  18000/23434          
c   -- var.elim.:  19000/23434          
c   -- var.elim.:  20000/23434          
c   -- var.elim.:  21000/23434          
c   -- var.elim.:  22000/23434          
c   -- var.elim.:  23000/23434          
c   -- var.elim.:  23434/23434          
c   -- var.elim.:  197/197          
c   -- var.elim.:  101/101          
c   -- subsuming                       
c   -- var.elim.:  1000/9300          
c   -- var.elim.:  2000/9300          
c   -- var.elim.:  3000/9300          
c   -- var.elim.:  4000/9300          
c   -- var.elim.:  5000/9300          
c   -- var.elim.:  6000/9300          
c   -- var.elim.:  7000/9300          
c   -- var.elim.:  8000/9300          
c   -- var.elim.:  9000/9300          
c   -- var.elim.:  9300/9300          
c   -- var.elim.:  468/468          
c   -- subsuming                       
c   -- var.elim.:  37/37          
c |         0 |  100068   342020 |      --       0       --      -- |     --   | -47920/22555
c |         0 |  100068   342020 |   40027       0        0     nan |  0.000 % |
c |       100 |  100068   342020 |   44029     100    15657   156.6 | 53.442 % |
c |       250 |  100068   342020 |   48432     250    43744   175.0 | 53.442 % |
c |       475 |  100068   342020 |   53276     475    76670   161.4 | 53.442 % |
c |       812 |  100068   342020 |   58603     812   146438   180.3 | 53.442 % |
c |      1318 |  100068   342020 |   64464    1318   239362   181.6 | 53.442 % |
c |      2077 |  100068   342020 |   70910    2077   365670   176.1 | 53.442 % |
c |      3216 |  100068   342020 |   78001    3216   605515   188.3 | 53.442 % |
c |      4924 |   99972   341119 |   85719    4919  1029027   209.2 | 53.631 % |
c |      7486 |   99570   337001 |   93912    7459  1571824   210.7 | 54.448 % |
c |     11330 |   98933   331022 |  102642   11243  2450783   218.0 | 55.685 % |
c |     17096 |   98235   324232 |  112110   16931  4111346   242.8 | 57.180 % |
c ==============================================================================
c (current CPU-time: 351.617 s)
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24549 |   97683   318708 |   29304   24303  6256013   257.4 | 57.180 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9179          
c   -- var.elim.:  2000/9179          
c   -- var.elim.:  3000/9179          
c   -- var.elim.:  4000/9179          
c   -- var.elim.:  5000/9179          
c   -- var.elim.:  6000/9179          
c   -- var.elim.:  7000/9179          
c   -- var.elim.:  8000/9179          
c   -- var.elim.:  9000/9179          
c   -- var.elim.:  9179/9179          
c   -- var.elim.:  113/113          
c |     24549 |   97638   318390 |      --   24303       --      -- |     --   | -35/-135
c |     24549 |   97638   318390 |   39055   22121  4158439   188.0 | 57.180 % |
c |     24649 |   97638   318390 |   42960   22221  4185424   188.4 | 58.486 % |
c |     24799 |   97634   318340 |   47254   22370  4227976   189.0 | 58.495 % |
c |     25024 |   97634   318340 |   51980   22595  4285965   189.7 | 58.495 % |
c |     25361 |   97598   318041 |   57157   22923  4418205   192.7 | 58.572 % |
c |     25867 |   97418   316399 |   62757   23416  4516415   192.9 | 58.957 % |
c |     26626 |   97412   316319 |   69028   24158  4753388   196.8 | 58.970 % |
c |     27768 |   97002   312545 |   75611   25258  5052886   200.1 | 59.848 % |
c |     29476 |   96858   311214 |   83049   26911  5661783   210.4 | 60.152 % |
c |     32038 |   96568   308432 |   91080   29415  6525134   221.8 | 60.768 % |
c |     35882 |   96155   304660 |   99760   33175  7739601   233.3 | 61.624 % |
c ==============================================================================
c (current CPU-time: 431.103 s)
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     36393 |  104864   327971 |   31459   33681  7904298   234.7 | 61.624 % |
c   -- subsuming                       
c   -- var.elim.:  1000/16187          
c   -- var.elim.:  2000/16187          
c   -- var.elim.:  3000/16187          
c   -- var.elim.:  4000/16187          
c   -- var.elim.:  5000/16187          
c   -- var.elim.:  6000/16187          
c   -- var.elim.:  7000/16187          
c   -- var.elim.:  8000/16187          
c   -- var.elim.:  9000/16187          
c   -- var.elim.:  10000/16187          
c   -- var.elim.:  11000/16187          
c   -- var.elim.:  12000/16187          
c   -- var.elim.:  13000/16187          
c   -- var.elim.:  14000/16187          
c   -- var.elim.:  15000/16187          
c   -- var.elim.:  16000/16187          
c   -- var.elim.:  16187/16187          
c   -- var.elim.:  1000/6009          
c   -- var.elim.:  2000/6009          
c   -- var.elim.:  3000/6009          
c   -- var.elim.:  4000/6009          
c   -- var.elim.:  5000/6009          
c   -- var.elim.:  6000/6009          
c   -- var.elim.:  6009/6009          
c   -- var.elim.:  474/474          
c   -- subsuming                       
c   -- var.elim.:  1000/5915          
c   -- var.elim.:  2000/5915          
c   -- var.elim.:  3000/5915          
c   -- var.elim.:  4000/5915          
c   -- var.elim.:  5000/5915          
c   -- var.elim.:  5915/5915          
c   -- var.elim.:  75/75          
c |     36393 |   96259   313503 |      --   33681       --      -- |     --   | -8597/-14451
c |     36393 |   96259   313503 |   38503   33681  7904298   234.7 | 61.624 % |
c |     36493 |   96259   313503 |   42353   33781  7919836   234.4 | 69.274 % |
c |     36645 |   96259   313503 |   46589   33933  7971433   234.9 | 69.274 % |
c |     36870 |   96178   310989 |   51205   33710  7891172   234.1 | 69.397 % |
c |     37207 |   96098   310293 |   56278   34036  8009789   235.3 | 69.523 % |
c |     37713 |   96098   310293 |   61906   34542  8138161   235.6 | 69.523 % |
c |     38474 |   96098   310293 |   68097   35303  8467852   239.9 | 69.523 % |
c |     39615 |   96046   309811 |   74866   36436  8854880   243.0 | 69.609 % |
c |     41323 |   95921   308522 |   82246   38111  9400111   246.7 | 69.814 % |
c |     43885 |   95774   307084 |   90332   40641 10403797   256.0 | 70.057 % |
c |     47729 |   95669   306030 |   99256   44423 11797957   265.6 | 70.231 % |
c |     53496 |   95478   304078 |  108963   50134 13994957   279.2 | 70.542 % |
c |     62145 |   94702   296456 |  118886   58566 17419422   297.4 | 71.817 % |
c |     75119 |   94373   293112 |  130320   71330 22756519   319.0 | 72.364 % |
c |     94580 |   93751   287234 |  142407   90526 32398010   357.9 | 73.406 % |
c ==============================================================================
c (current CPU-time: 996.939 s)
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    101577 |   93769   286507 |   28130   97485 35608814   365.3 | 73.406 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7657          
c   -- var.elim.:  2000/7657          
c   -- var.elim.:  3000/7657          
c   -- var.elim.:  4000/7657          
c   -- var.elim.:  5000/7657          
c   -- var.elim.:  6000/7657          
c   -- var.elim.:  7000/7657          
c   -- var.elim.:  7657/7657          
c   -- var.elim.:  303/303          
c |    101577 |   93632   285473 |      --   97485       --      -- |     --   | -127/-760
c |    101577 |   93632   285473 |   37452   80919 17807810   220.1 | 73.406 % |
c |    101678 |   93632   285473 |   41198   19960  2465168   123.5 | 73.684 % |
c |    101828 |   93632   285473 |   45317   20110  2524397   125.5 | 73.684 % |
c |    102053 |   93632   285473 |   49849   20335  2617067   128.7 | 73.684 % |
c |    102390 |   93588   285070 |   54808   20669  2740673   132.6 | 73.756 % |
c |    102896 |   93588   285070 |   60289   21175  2948787   139.3 | 73.756 % |
c |    103657 |   93544   284432 |   66287   21929  3179534   145.0 | 73.828 % |
c |    104796 |   93544   284432 |   72916   23068  3605897   156.3 | 73.828 % |
c |    106504 |   93294   281973 |   79993   24753  4282814   173.0 | 74.238 % |
c |    109066 |   93294   281973 |   87992   27315  5331356   195.2 | 74.238 % |
c |    112910 |   93258   281575 |   96754   31135  6655167   213.8 | 74.296 % |
c |    118676 |   93226   281267 |  106393   36899  8882125   240.7 | 74.347 % |
c |    127326 |   93102   280033 |  116877   45532 12545505   275.5 | 74.556 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 C1013 -C1012 -C1011 -C1010 C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 C602 -C601 -C600 -C599 C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 C489 -C488 -C487 -C486 -C485 -C484 -C483 -C48#### 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): 1.03 1.01 0.93 2/54 18419
Raw data (stat): 18419 (runsolver) R 18418 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480479738 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9296 0 0 0 958 40 0 0 25 0 1 0 480479738 40292352 8720 4294967295 134512640 134672761 3221224560 3221222448 134566554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9837 8720 603 41 0 9796 0
vsize: 39348
[startup+20.0021 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9302 0 0 0 1958 40 0 0 25 0 1 0 480479738 40292352 8726 4294967295 134512640 134672761 3221224560 3221223088 134606420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9837 8726 603 41 0 9796 0
vsize: 39348
[startup+30.0025 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9303 0 0 0 2958 40 0 0 25 0 1 0 480479738 40292352 8727 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9837 8727 603 41 0 9796 0
vsize: 39348
[startup+40.0027 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9304 0 0 0 3958 40 0 0 25 0 1 0 480479738 40292352 8728 4294967295 134512640 134672761 3221224560 3221222992 134604097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9837 8728 603 41 0 9796 0
vsize: 39348
[startup+50.0034 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9305 0 0 0 4957 41 0 0 25 0 1 0 480479738 40292352 8729 4294967295 134512640 134672761 3221224560 3221222076 134566513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9837 8729 603 41 0 9796 0
vsize: 39348
[startup+60.0026 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9306 0 0 0 5957 41 0 0 25 0 1 0 480479738 40292352 8730 4294967295 134512640 134672761 3221224560 3221223040 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9837 8730 603 41 0 9796 0
vsize: 39348
[startup+70.0071 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9312 0 0 0 6957 41 0 0 25 0 1 0 480479738 40292352 8736 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9837 8736 603 41 0 9796 0
vsize: 39348
[startup+80.0072 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9314 0 0 0 7957 41 0 0 25 0 1 0 480479738 40292352 8738 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9837 8738 603 41 0 9796 0
vsize: 39348
[startup+90.0065 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9320 0 0 0 8957 41 0 0 25 0 1 0 480479738 40423424 8744 4294967295 134512640 134672761 3221224560 3221223056 134644277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9869 8744 603 41 0 9828 0
vsize: 39476
[startup+100.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9353 0 0 0 9957 41 0 0 25 0 1 0 480479738 40685568 8777 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8777 603 41 0 9892 0
vsize: 39732
[startup+110.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9354 0 0 0 10958 41 0 0 25 0 1 0 480479738 40685568 8778 4294967295 134512640 134672761 3221224560 3221222816 134621242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8778 603 41 0 9892 0
vsize: 39732
[startup+120.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9355 0 0 0 11958 41 0 0 25 0 1 0 480479738 40685568 8779 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8779 603 41 0 9892 0
vsize: 39732
[startup+130.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9358 0 0 0 12958 41 0 0 25 0 1 0 480479738 40685568 8782 4294967295 134512640 134672761 3221224560 3221223088 134606937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8782 603 41 0 9892 0
vsize: 39732
[startup+140.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9361 0 0 0 13958 41 0 0 25 0 1 0 480479738 40685568 8785 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8785 603 41 0 9892 0
vsize: 39732
[startup+150.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9362 0 0 0 14959 41 0 0 25 0 1 0 480479738 40685568 8786 4294967295 134512640 134672761 3221224560 3221223056 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8786 603 41 0 9892 0
vsize: 39732
[startup+160.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9365 0 0 0 15958 41 0 0 25 0 1 0 480479738 40685568 8789 4294967295 134512640 134672761 3221224560 3221223152 134607935 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8789 603 41 0 9892 0
vsize: 39732
[startup+170.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18419
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9367 0 0 0 16959 41 0 0 25 0 1 0 480479738 40685568 8791 4294967295 134512640 134672761 3221224560 3221223056 134644251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8791 603 41 0 9892 0
vsize: 39732
[startup+180.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9394 0 0 0 17958 42 0 0 25 0 1 0 480479738 40693760 8772 4294967295 134512640 134672761 3221224560 3221223008 134643969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9935 8772 603 41 0 9894 0
vsize: 39740
[startup+190.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9394 0 0 0 18959 42 0 0 25 0 1 0 480479738 40693760 8772 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9935 8772 603 41 0 9894 0
vsize: 39740
[startup+200.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9394 0 0 0 19959 42 0 0 25 0 1 0 480479738 40693760 8772 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9935 8772 603 41 0 9894 0
vsize: 39740
[startup+210.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9704 0 0 0 20958 43 0 0 25 0 1 0 480479738 42545152 9036 4294967295 134512640 134672761 3221224560 3221222960 134604652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10387 9036 603 41 0 10346 0
vsize: 41548
[startup+220.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9704 0 0 0 21958 43 0 0 25 0 1 0 480479738 42545152 9036 4294967295 134512640 134672761 3221224560 3221223120 134607998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10387 9036 603 41 0 10346 0
vsize: 41548
[startup+230.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9704 0 0 0 22959 43 0 0 25 0 1 0 480479738 42545152 9036 4294967295 134512640 134672761 3221224560 3221223104 134621071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10387 9036 603 41 0 10346 0
vsize: 41548
[startup+240.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9704 0 0 0 23959 43 0 0 25 0 1 0 480479738 42545152 9036 4294967295 134512640 134672761 3221224560 3221223104 134621081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10387 9036 603 41 0 10346 0
vsize: 41548
[startup+250.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 9704 0 0 0 24959 43 0 0 25 0 1 0 480479738 40300544 8732 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9839 8732 603 41 0 9798 0
vsize: 39356
[startup+260.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 10072 0 0 0 25958 44 0 0 25 0 1 0 480479738 40693760 8810 4294967295 134512640 134672761 3221224560 3221223696 134566155 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9935 8810 603 41 0 9894 0
vsize: 39740
[startup+270.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 10766 0 0 0 26956 46 0 0 25 0 1 0 480479738 43429888 9504 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10603 9504 603 41 0 10562 0
vsize: 42412
[startup+280.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 11247 0 0 0 27955 47 0 0 25 0 1 0 480479738 45408256 9985 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11086 9985 603 41 0 11045 0
vsize: 44344
[startup+290.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 11933 0 0 0 28953 49 0 0 25 0 1 0 480479738 48271360 10671 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11785 10671 603 41 0 11744 0
vsize: 47140
[startup+300.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 12363 0 0 0 29952 50 0 0 25 0 1 0 480479738 50081792 11101 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12227 11101 603 41 0 12186 0
vsize: 48908
[startup+310.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 13127 0 0 0 30950 52 0 0 25 0 1 0 480479738 53182464 11865 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12984 11865 603 41 0 12943 0
vsize: 51936
[startup+320.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 13779 0 0 0 31949 53 0 0 25 0 1 0 480479738 55906304 12517 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13649 12517 603 41 0 13608 0
vsize: 54596
[startup+330.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 14520 0 0 0 32948 55 0 0 25 0 1 0 480479738 58920960 13258 4294967295 134512640 134672761 3221224560 3221223200 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14385 13258 603 41 0 14344 0
vsize: 57540
[startup+340.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 15159 0 0 0 33946 57 0 0 25 0 1 0 480479738 61509632 13897 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15017 13897 603 41 0 14976 0
vsize: 60068
[startup+350.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 15770 0 0 0 34945 58 0 0 25 0 1 0 480479738 63975424 14508 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15619 14508 603 41 0 15578 0
vsize: 62476
[startup+360.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 17877 0 0 0 35934 68 0 0 25 0 1 0 480479738 69373952 15413 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16937 15413 603 41 0 16896 0
vsize: 67748
[startup+370.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 17877 0 0 0 36934 68 0 0 25 0 1 0 480479738 67211264 15123 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16409 15123 603 41 0 16368 0
vsize: 65636
[startup+380.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 17877 0 0 0 37934 68 0 0 25 0 1 0 480479738 67211264 15123 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16409 15123 603 41 0 16368 0
vsize: 65636
[startup+390.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 17879 0 0 0 38934 68 0 0 25 0 1 0 480479738 67211264 15125 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16409 15125 603 41 0 16368 0
vsize: 65636
[startup+400.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 17882 0 0 0 39935 68 0 0 25 0 1 0 480479738 67211264 15128 4294967295 134512640 134672761 3221224560 3221223704 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16409 15128 603 41 0 16368 0
vsize: 65636
[startup+410.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 17928 0 0 0 40935 69 0 0 25 0 1 0 480479738 67457024 15174 4294967295 134512640 134672761 3221224560 3221223008 134566562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16469 15174 603 41 0 16428 0
vsize: 65876
[startup+420.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 18508 0 0 0 41934 69 0 0 25 0 1 0 480479738 69881856 15754 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17061 15754 603 41 0 17020 0
vsize: 68244
[startup+430.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 19115 0 0 0 42933 71 0 0 25 0 1 0 480479738 72478720 16361 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17695 16361 603 41 0 17654 0
vsize: 70780
[startup+440.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 21185 0 0 0 43922 82 0 0 25 0 1 0 480479738 75337728 17063 4294967295 134512640 134672761 3221224560 3221223104 134621041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18393 17063 603 41 0 18352 0
vsize: 73572
[startup+450.02 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 21230 0 0 0 44873 130 0 0 25 0 1 0 480479738 72970240 16773 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17815 16773 603 41 0 17774 0
vsize: 71260
[startup+460.02 s]
Raw data (loadavg): 1.14 1.03 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 21230 0 0 0 45873 130 0 0 25 0 1 0 480479738 72970240 16773 4294967295 134512640 134672761 3221224560 3221223008 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17815 16773 603 41 0 17774 0
vsize: 71260
[startup+470.021 s]
Raw data (loadavg): 1.12 1.03 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 21230 0 0 0 46873 131 0 0 25 0 1 0 480479738 72970240 16773 4294967295 134512640 134672761 3221224560 3221223008 134643612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17815 16773 603 41 0 17774 0
vsize: 71260
[startup+480.021 s]
Raw data (loadavg): 1.10 1.03 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 21520 0 0 0 47872 132 0 0 25 0 1 0 480479738 75141120 17063 4294967295 134512640 134672761 3221224560 3221222112 134566490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18345 17063 603 41 0 18304 0
vsize: 73380
[startup+490.021 s]
Raw data (loadavg): 1.08 1.03 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 21520 0 0 0 48872 132 0 0 25 0 1 0 480479738 72970240 16773 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17815 16773 603 41 0 17774 0
vsize: 71260
[startup+500.022 s]
Raw data (loadavg): 1.07 1.03 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 21537 0 0 0 49872 132 0 0 25 0 1 0 480479738 73101312 16790 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17847 16790 603 41 0 17806 0
vsize: 71388
[startup+510.021 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 22086 0 0 0 50870 133 0 0 25 0 1 0 480479738 75313152 17339 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18387 17339 603 41 0 18346 0
vsize: 73548
[startup+520.022 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 22621 0 0 0 51869 134 0 0 25 0 1 0 480479738 77541376 17874 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18931 17874 603 41 0 18890 0
vsize: 75724
[startup+530.023 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 23206 0 0 0 52868 135 0 0 25 0 1 0 480479738 79872000 18459 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19500 18459 603 41 0 19459 0
vsize: 78000
[startup+540.022 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 24140 0 0 0 53866 138 0 0 25 0 1 0 480479738 83742720 19393 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20445 19393 603 41 0 20404 0
vsize: 81780
[startup+550.023 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 24740 0 0 0 54864 140 0 0 25 0 1 0 480479738 86204416 19993 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21046 19993 603 41 0 21005 0
vsize: 84184
[startup+560.023 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 25383 0 0 0 55862 142 0 0 25 0 1 0 480479738 88805376 20636 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21681 20636 603 41 0 21640 0
vsize: 86724
[startup+570.023 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 25989 0 0 0 56862 143 0 0 25 0 1 0 480479738 91283456 21242 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22286 21242 603 41 0 22245 0
vsize: 89144
[startup+580.023 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 26656 0 0 0 57860 144 0 0 25 0 1 0 480479738 93990912 21909 4294967295 134512640 134672761 3221224560 3221223684 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22947 21909 603 41 0 22906 0
vsize: 91788
[startup+590.023 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 27184 0 0 0 58859 146 0 0 25 0 1 0 480479738 96210944 22437 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23489 22437 603 41 0 23448 0
vsize: 93956
[startup+600.023 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 27752 0 0 0 59858 147 0 0 25 0 1 0 480479738 98541568 23005 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24058 23005 603 41 0 24017 0
vsize: 96232
[startup+610.024 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 28172 0 0 0 60857 148 0 0 25 0 1 0 480479738 100200448 23425 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24463 23425 603 41 0 24422 0
vsize: 97852
[startup+620.024 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 28752 0 0 0 61856 149 0 0 25 0 1 0 480479738 102518784 24005 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25029 24005 603 41 0 24988 0
vsize: 100116
[startup+630.024 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 29411 0 0 0 62854 151 0 0 25 0 1 0 480479738 105332736 24664 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25716 24664 603 41 0 25675 0
vsize: 102864
[startup+640.024 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 29878 0 0 0 63854 152 0 0 25 0 1 0 480479738 107110400 25131 4294967295 134512640 134672761 3221224560 3221223704 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26150 25131 603 41 0 26109 0
vsize: 104600
[startup+650.025 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 30367 0 0 0 64853 153 0 0 25 0 1 0 480479738 109191168 25620 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26658 25620 603 41 0 26617 0
vsize: 106632
[startup+660.024 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 31015 0 0 0 65852 155 0 0 25 0 1 0 480479738 111845376 26268 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27306 26268 603 41 0 27265 0
vsize: 109224
[startup+670.026 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 31613 0 0 0 66851 156 0 0 25 0 1 0 480479738 114249728 26866 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27893 26866 603 41 0 27852 0
vsize: 111572
[startup+680.026 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 32199 0 0 0 67849 157 0 0 25 0 1 0 480479738 116609024 27452 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28469 27452 603 41 0 28428 0
vsize: 113876
[startup+690.025 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 32900 0 0 0 68848 159 0 0 25 0 1 0 480479738 119537664 28153 4294967295 134512640 134672761 3221224560 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29184 28153 603 41 0 29143 0
vsize: 116736
[startup+700.026 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 33334 0 0 0 69847 160 0 0 25 0 1 0 480479738 121262080 28587 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29605 28587 603 41 0 29564 0
vsize: 118420
[startup+710.026 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 33881 0 0 0 70846 161 0 0 25 0 1 0 480479738 123535360 29134 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30160 29134 603 41 0 30119 0
vsize: 120640
[startup+720.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 34427 0 0 0 71846 162 0 0 25 0 1 0 480479738 126001152 29680 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30762 29680 603 41 0 30721 0
vsize: 123048
[startup+730.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 35057 0 0 0 72845 163 0 0 25 0 1 0 480479738 128585728 30310 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31393 30310 603 41 0 31352 0
vsize: 125572
[startup+740.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 35614 0 0 0 73843 165 0 0 25 0 1 0 480479738 130879488 30867 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31953 30867 603 41 0 31912 0
vsize: 127812
[startup+750.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 35997 0 0 0 74843 166 0 0 25 0 1 0 480479738 132460544 31250 4294967295 134512640 134672761 3221224560 3221223600 134612862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32339 31253 603 41 0 32298 0
vsize: 129356
[startup+760.026 s]
Raw data (loadavg): 1.00 1.00 0.94 3/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 36620 0 0 0 75841 167 0 0 25 0 1 0 480479738 135041024 31873 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32969 31873 603 41 0 32928 0
vsize: 131876
[startup+770.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 37136 0 0 0 76840 168 0 0 25 0 1 0 480479738 137076736 32389 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33466 32389 603 41 0 33425 0
vsize: 133864
[startup+780.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 37563 0 0 0 77839 169 0 0 25 0 1 0 480479738 138887168 32816 4294967295 134512640 134672761 3221224560 3221223748 134610770 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33908 32816 603 41 0 33867 0
vsize: 135632
[startup+790.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 37717 0 0 0 78839 170 0 0 25 0 1 0 480479738 139403264 32970 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34034 32970 603 41 0 33993 0
vsize: 136136
[startup+800.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 38282 0 0 0 79838 171 0 0 25 0 1 0 480479738 141713408 33535 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34598 33535 603 41 0 34557 0
vsize: 138392
[startup+810.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 38641 0 0 0 80837 172 0 0 25 0 1 0 480479738 143273984 33894 4294967295 134512640 134672761 3221224560 3221223684 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34979 33894 603 41 0 34938 0
vsize: 139916
[startup+820.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 39284 0 0 0 81836 174 0 0 25 0 1 0 480479738 145846272 34537 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35607 34537 603 41 0 35566 0
vsize: 142428
[startup+830.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 39843 0 0 0 82835 175 0 0 25 0 1 0 480479738 148185088 35096 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36178 35096 603 41 0 36137 0
vsize: 144712
[startup+840.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 40243 0 0 0 83834 176 0 0 25 0 1 0 480479738 149843968 35496 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36583 35496 603 41 0 36542 0
vsize: 146332
[startup+850.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 41072 0 0 0 84832 178 0 0 25 0 1 0 480479738 153182208 36325 4294967295 134512640 134672761 3221224560 3221223408 134604034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37398 36325 603 41 0 37357 0
vsize: 149592
[startup+860.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 41429 0 0 0 85832 178 0 0 25 0 1 0 480479738 154595328 36682 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37743 36682 603 41 0 37702 0
vsize: 150972
[startup+870.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 41861 0 0 0 86831 179 0 0 25 0 1 0 480479738 156459008 37114 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38198 37114 603 41 0 38157 0
vsize: 152792
[startup+880.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 42750 0 0 0 87830 181 0 0 25 0 1 0 480479738 159993856 38003 4294967295 134512640 134672761 3221224560 3221222448 134566704 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39061 38003 603 41 0 39020 0
vsize: 156244
[startup+890.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 43155 0 0 0 88829 182 0 0 25 0 1 0 480479738 161673216 38408 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39471 38408 603 41 0 39430 0
vsize: 157884
[startup+900.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 44822 0 0 0 89825 186 0 0 25 0 1 0 480479738 168484864 40075 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41134 40075 603 41 0 41093 0
vsize: 164536
[startup+910.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 45169 0 0 0 90824 187 0 0 25 0 1 0 480479738 169893888 40422 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41478 40422 603 41 0 41437 0
vsize: 165912
[startup+920.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 45377 0 0 0 91824 187 0 0 25 0 1 0 480479738 170815488 40630 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41703 40630 603 41 0 41662 0
vsize: 166812
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 45934 0 0 0 92823 189 0 0 25 0 1 0 480479738 172998656 41187 4294967295 134512640 134672761 3221224560 3221223600 134614328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42236 41187 603 41 0 42195 0
vsize: 168944
[startup+940.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 46467 0 0 0 93822 190 0 0 25 0 1 0 480479738 175300608 41720 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42798 41720 603 41 0 42757 0
vsize: 171192
[startup+950.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 46972 0 0 0 94821 191 0 0 25 0 1 0 480479738 177254400 42225 4294967295 134512640 134672761 3221224560 3221223704 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43275 42225 603 41 0 43234 0
vsize: 173100
[startup+960.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 47341 0 0 0 95820 192 0 0 25 0 1 0 480479738 178769920 42594 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43645 42594 603 41 0 43604 0
vsize: 174580
[startup+970.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 48111 0 0 0 96820 192 0 0 25 0 1 0 480479738 181936128 43364 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44418 43364 603 41 0 44377 0
vsize: 177672
[startup+980.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 48703 0 0 0 97819 194 0 0 25 0 1 0 480479738 184332288 43956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45003 43956 603 41 0 44962 0
vsize: 180012
[startup+990.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 49370 0 0 0 98817 196 0 0 25 0 1 0 480479738 187142144 44623 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45689 44623 603 41 0 45648 0
vsize: 182756
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 51981 0 0 0 99798 215 0 0 25 0 1 0 480479738 190345216 45308 4294967295 134512640 134672761 3221224560 3221223104 134621062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46471 45308 603 41 0 46430 0
vsize: 185884
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 51989 0 0 0 100797 216 0 0 25 0 1 0 480479738 188739584 45011 4294967295 134512640 134672761 3221224560 3221223008 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46079 45011 603 41 0 46038 0
vsize: 184316
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 101797 216 0 0 25 0 1 0 480479738 189648896 45159 4294967295 134512640 134672761 3221224560 3221223656 134616183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46301 45159 603 41 0 46260 0
vsize: 185204
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 102797 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 103797 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 104797 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 105797 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 106797 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 107797 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 108798 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 109798 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 110798 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 111798 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 112798 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223696 134614524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 113798 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 114799 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 115799 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 116799 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 117799 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 118799 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 18421
Raw data (stat): 18419 (minisat+) R 18418 10614 10613 0 -1 0 52145 0 0 0 119800 216 0 0 25 0 1 0 480479738 189124608 45079 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46173 45079 603 41 0 46132 0
vsize: 184692
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 18421
Raw data (stat): 18419 (minisat+) Z 18418 10614 10613 0 -1 12 52146 0 0 0 119800 228 0 0 25 0 1 0 480479738 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.16
CPU time (s): 1200.29
CPU user time (s): 1198
CPU system time (s): 2.28665
CPU usage (%): 100.011
Max. virtual memory (Kb): 185884
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####