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-4.opb
MD5SUM	b85a90571dde4fe12541342d5605d680
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.1
Number of variables	1150
Total number of constraints	80258
Number of constraints which are clauses	80258
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 5631

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        908860 kB
Buffers:         35448 kB
Cached:          65564 kB
SwapCached:       4932 kB
Active:          57940 kB
Inactive:        50876 kB
HighTotal:      131008 kB
HighFree:        61740 kB
LowTotal:       903652 kB
LowFree:        847120 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11468 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:24:02 (client local time) WITH STATUS 10 IN 1209.97 SECONDS
stats: 4097 7 1209.97 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80258 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 |   80258   160516 |   24077       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   80258   160516 |   32103       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.21436 s)
c ==============================================================================
c [1mFound solution: -36[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 |  148150   319784 |   44444       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/46206          
c   -- var.elim.:  2000/46206          
c   -- var.elim.:  3000/46206          
c   -- var.elim.:  4000/46206          
c   -- var.elim.:  5000/46206          
c   -- var.elim.:  6000/46206          
c   -- var.elim.:  7000/46206          
c   -- var.elim.:  8000/46206          
c   -- var.elim.:  9000/46206          
c   -- var.elim.:  10000/46206          
c   -- var.elim.:  11000/46206          
c   -- var.elim.:  12000/46206          
c   -- var.elim.:  13000/46206          
c   -- var.elim.:  14000/46206          
c   -- var.elim.:  15000/46206          
c   -- var.elim.:  16000/46206          
c   -- var.elim.:  17000/46206          
c   -- var.elim.:  18000/46206          
c   -- var.elim.:  19000/46206          
c   -- var.elim.:  20000/46206          
c   -- var.elim.:  21000/46206          
c   -- var.elim.:  22000/46206          
c   -- var.elim.:  23000/46206          
c   -- var.elim.:  24000/46206          
c   -- var.elim.:  25000/46206          
c   -- var.elim.:  26000/46206          
c   -- var.elim.:  27000/46206          
c   -- var.elim.:  28000/46206          
c   -- var.elim.:  29000/46206          
c   -- var.elim.:  30000/46206          
c   -- var.elim.:  31000/46206          
c   -- var.elim.:  32000/46206          
c   -- var.elim.:  33000/46206          
c   -- var.elim.:  34000/46206          
c   -- var.elim.:  35000/46206          
c   -- var.elim.:  36000/46206          
c   -- var.elim.:  37000/46206          
c   -- var.elim.:  38000/46206          
c   -- var.elim.:  39000/46206          
c   -- var.elim.:  40000/46206          
c   -- var.elim.:  41000/46206          
c   -- var.elim.:  42000/46206          
c   -- var.elim.:  43000/46206          
c   -- var.elim.:  44000/46206          
c   -- var.elim.:  45000/46206          
c   -- var.elim.:  46000/46206          
c   -- var.elim.:  46206/46206          
c   -- var.elim.:  1000/23428          
c   -- var.elim.:  2000/23428          
c   -- var.elim.:  3000/23428          
c   -- var.elim.:  4000/23428          
c   -- var.elim.:  5000/23428          
c   -- var.elim.:  6000/23428          
c   -- var.elim.:  7000/23428          
c   -- var.elim.:  8000/23428          
c   -- var.elim.:  9000/23428          
c   -- var.elim.:  10000/23428          
c   -- var.elim.:  11000/23428          
c   -- var.elim.:  12000/23428          
c   -- var.elim.:  13000/23428          
c   -- var.elim.:  14000/23428          
c   -- var.elim.:  15000/23428          
c   -- var.elim.:  16000/23428          
c   -- var.elim.:  17000/23428          
c   -- var.elim.:  18000/23428          
c   -- var.elim.:  19000/23428          
c   -- var.elim.:  20000/23428          
c   -- var.elim.:  21000/23428          
c   -- var.elim.:  22000/23428          
c   -- var.elim.:  23000/23428          
c   -- var.elim.:  23428/23428          
c   -- var.elim.:  188/188          
c   -- var.elim.:  105/105          
c   -- subsuming                       
c   -- var.elim.:  1000/9258          
c   -- var.elim.:  2000/9258          
c   -- var.elim.:  3000/9258          
c   -- var.elim.:  4000/9258          
c   -- var.elim.:  5000/9258          
c   -- var.elim.:  6000/9258          
c   -- var.elim.:  7000/9258          
c   -- var.elim.:  8000/9258          
c   -- var.elim.:  9000/9258          
c   -- var.elim.:  9258/9258          
c   -- var.elim.:  233/233          
c |         0 |  100145   339962 |      --       0       --      -- |     --   | -47999/20196
c |         0 |  100145   339962 |   40058       0        0     nan |  0.000 % |
c |       101 |  100145   339962 |   44063     101    26740   264.8 | 53.613 % |
c |       251 |  100145   339962 |   48470     251    56243   224.1 | 53.613 % |
c |       476 |  100145   339962 |   53317     476    93082   195.6 | 53.613 % |
c |       813 |  100145   339962 |   58648     813   160830   197.8 | 53.613 % |
c |      1319 |  100145   339962 |   64513    1319   286563   217.3 | 53.613 % |
c |      2078 |  100103   339516 |   70935    2073   446461   215.4 | 53.703 % |
c |      3218 |  100071   339153 |   78004    3207   670779   209.2 | 53.771 % |
c |      4926 |   99976   338305 |   85722    4907  1067884   217.6 | 53.938 % |
c |      7488 |   99869   337260 |   94194    7465  1689699   226.3 | 54.156 % |
c |     11332 |   99613   334772 |  103348   11282  2769034   245.4 | 54.661 % |
c |     17098 |   99150   330364 |  113154   16994  4811060   283.1 | 55.603 % |
c ==============================================================================
c (current CPU-time: 339.141 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 |     23383 |  102323   335785 |   30696   23191  6877433   296.6 | 55.603 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13239          
c   -- var.elim.:  2000/13239          
c   -- var.elim.:  3000/13239          
c   -- var.elim.:  4000/13239          
c   -- var.elim.:  5000/13239          
c   -- var.elim.:  6000/13239          
c   -- var.elim.:  7000/13239          
c   -- var.elim.:  8000/13239          
c   -- var.elim.:  9000/13239          
c   -- var.elim.:  10000/13239          
c   -- var.elim.:  11000/13239          
c   -- var.elim.:  12000/13239          
c   -- var.elim.:  13000/13239          
c   -- var.elim.:  13239/13239          
c   -- var.elim.:  1000/2916          
c   -- var.elim.:  2000/2916          
c   -- var.elim.:  2916/2916          
c   -- var.elim.:  185/185          
c |     23383 |   98663   329745 |      --   23191       --      -- |     --   | -3653/-4584
c |     23383 |   98663   329745 |   39465   23191  6877433   296.6 | 55.603 % |
c |     23484 |   98663   329745 |   43411   23292  6893956   296.0 | 58.857 % |
c |     23634 |   98663   329745 |   47752   23442  6960984   296.9 | 58.857 % |
c |     23860 |   98625   329339 |   52507   21903  4500459   205.5 | 58.934 % |
c |     24197 |   98591   329050 |   57738   22237  4582627   206.1 | 59.003 % |
c |     24703 |   98479   327931 |   63440   22725  4716276   207.5 | 59.231 % |
c |     25462 |   98479   327931 |   69784   23484  5027673   214.1 | 59.231 % |
c |     26601 |   98363   326856 |   76672   24604  5360358   217.9 | 59.467 % |
c |     28310 |   98095   324181 |   84110   26263  5863820   223.3 | 60.011 % |
c |     30872 |   97752   320937 |   92197   28769  6811574   236.8 | 60.707 % |
c |     34716 |   97518   318757 |  101174   32581  8354092   256.4 | 61.182 % |
c |     40482 |   96998   313666 |  110698   38231 10300209   269.4 | 62.219 % |
c ==============================================================================
c (current CPU-time: 476.534 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 |     44440 |  106628   338105 |   31988   42122 11836463   281.0 | 62.219 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18858          
c   -- var.elim.:  2000/18858          
c   -- var.elim.:  3000/18858          
c   -- var.elim.:  4000/18858          
c   -- var.elim.:  5000/18858          
c   -- var.elim.:  6000/18858          
c   -- var.elim.:  7000/18858          
c   -- var.elim.:  8000/18858          
c   -- var.elim.:  9000/18858          
c   -- var.elim.:  10000/18858          
c   -- var.elim.:  11000/18858          
c   -- var.elim.:  12000/18858          
c   -- var.elim.:  13000/18858          
c   -- var.elim.:  14000/18858          
c   -- var.elim.:  15000/18858          
c   -- var.elim.:  16000/18858          
c   -- var.elim.:  17000/18858          
c   -- var.elim.:  18000/18858          
c   -- var.elim.:  18858/18858          
c   -- var.elim.:  1000/7266          
c   -- var.elim.:  2000/7266          
c   -- var.elim.:  3000/7266          
c   -- var.elim.:  4000/7266          
c   -- var.elim.:  5000/7266          
c   -- var.elim.:  6000/7266          
c   -- var.elim.:  7000/7266          
c   -- var.elim.:  7266/7266          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  1000/7142          
c   -- var.elim.:  2000/7142          
c   -- var.elim.:  3000/7142          
c   -- var.elim.:  4000/7142          
c   -- var.elim.:  5000/7142          
c   -- var.elim.:  6000/7142          
c   -- var.elim.:  7000/7142          
c   -- var.elim.:  7142/7142          
c   -- var.elim.:  47/47          
c |     44440 |   96842   320620 |      --   42122       --      -- |     --   | -9779/-17470
c |     44440 |   96842   320620 |   38736   41578 11589607   278.7 | 62.219 % |
c |     44540 |   96842   320620 |   42610   41678 11619993   278.8 | 68.567 % |
c |     44691 |   96842   320620 |   46871   41829 11671624   279.0 | 68.567 % |
c |     44916 |   96842   320620 |   51558   42054 11750419   279.4 | 68.567 % |
c |     45253 |   96807   320336 |   56694   42387 11861001   279.8 | 68.625 % |
c |     45759 |   96807   320336 |   62363   42893 12116882   282.5 | 68.625 % |
c |     46520 |   96807   320336 |   68599   43654 12443514   285.0 | 68.625 % |
c |     47659 |   96773   319994 |   75433   44786 13001616   290.3 | 68.683 % |
c |     49367 |   96731   319561 |   82940   46484 13737703   295.5 | 68.755 % |
c |     51929 |   96693   319136 |   91198   49045 15088557   307.6 | 68.817 % |
c |     55773 |   96487   317070 |  100104   52808 17025824   322.4 | 69.155 % |
c |     61539 |   95843   310529 |  109380   58450 19400113   331.9 | 70.233 % |
c ==============================================================================
c (current CPU-time: 670.686 s)
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     62827 |   97666   315841 |   29299   59738 19915307   333.4 | 70.233 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9944          
c   -- var.elim.:  2000/9944          
c   -- var.elim.:  3000/9944          
c   -- var.elim.:  4000/9944          
c   -- var.elim.:  5000/9944          
c   -- var.elim.:  6000/9944          
c   -- var.elim.:  7000/9944          
c   -- var.elim.:  8000/9944          
c   -- var.elim.:  9000/9944          
c   -- var.elim.:  9944/9944          
c   -- var.elim.:  1000/1741          
c   -- var.elim.:  1741/1741          
c |     62827 |   95876   312705 |      --   59738       --      -- |     --   | -1790/-3135
c |     62827 |   95876   312705 |   38350   59128 19567414   330.9 | 70.233 % |
c |     62927 |   95876   312705 |   42185   21701  5550618   255.8 | 70.292 % |
c |     63077 |   95876   312705 |   46403   21851  5579788   255.4 | 70.292 % |
c |     63302 |   95876   312705 |   51044   22076  5621480   254.6 | 70.292 % |
c |     63641 |   95876   312705 |   56148   22415  5699843   254.3 | 70.292 % |
c |     64147 |   95770   311573 |   61695   22918  5843835   255.0 | 70.470 % |
c |     64907 |   95770   311573 |   67864   23678  6062158   256.0 | 70.470 % |
c |     66046 |   95722   311065 |   74614   24812  6531334   263.2 | 70.552 % |
c |     67754 |   95589   309748 |   81961   26504  7169261   270.5 | 70.770 % |
c |     70317 |   95557   309415 |   90127   29055  7963581   274.1 | 70.825 % |
c |     74161 |   95377   307539 |   98953   32878  9249347   281.3 | 71.125 % |
c |     79928 |   95035   304225 |  108458   38572 11354119   294.4 | 71.699 % |
c |     88578 |   94406   298132 |  118514   47129 14584358   309.5 | 72.751 % |
c |    101552 |   93985   293739 |  129784   59991 19859086   331.0 | 73.447 % |
c |    121013 |   93181   285626 |  141541   79178 27453830   346.7 | 74.793 % |
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 -C#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.91 2/54 6094
Raw data (stat): 6094 (runsolver) R 6093 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422261153 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9299 0 0 0 959 39 0 0 25 0 1 0 422261153 40902656 8723 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9986 8723 603 41 0 9945 0
vsize: 39944
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9305 0 0 0 1958 40 0 0 25 0 1 0 422261153 40902656 8729 4294967295 134512640 134672761 3221224560 3221222992 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9986 8729 603 41 0 9945 0
vsize: 39944
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9306 0 0 0 2958 40 0 0 25 0 1 0 422261153 40902656 8730 4294967295 134512640 134672761 3221224560 3221222816 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9986 8730 603 41 0 9945 0
vsize: 39944
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9307 0 0 0 3957 40 0 0 25 0 1 0 422261153 40902656 8731 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9986 8731 603 41 0 9945 0
vsize: 39944
[startup+50.0037 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9308 0 0 0 4956 40 0 0 25 0 1 0 422261153 40902656 8732 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9986 8732 603 41 0 9945 0
vsize: 39944
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9309 0 0 0 5956 40 0 0 25 0 1 0 422261153 40902656 8733 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9986 8733 603 41 0 9945 0
vsize: 39944
[startup+70.0047 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9317 0 0 0 6955 40 0 0 25 0 1 0 422261153 40902656 8741 4294967295 134512640 134672761 3221224560 3221222816 134621164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9986 8741 603 41 0 9945 0
vsize: 39944
[startup+80.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9319 0 0 0 7955 41 0 0 25 0 1 0 422261153 40902656 8743 4294967295 134512640 134672761 3221224560 3221222176 134566712 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9986 8743 603 41 0 9945 0
vsize: 39944
[startup+90.0053 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9324 0 0 0 8955 41 0 0 25 0 1 0 422261153 41033728 8748 4294967295 134512640 134672761 3221224560 3221223152 134607772 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10018 8748 603 41 0 9977 0
vsize: 40072
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9357 0 0 0 9954 42 0 0 25 0 1 0 422261153 41295872 8781 4294967295 134512640 134672761 3221224560 3221222028 134566502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10082 8781 603 41 0 10041 0
vsize: 40328
[startup+110.006 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6094
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9358 0 0 0 10953 42 0 0 25 0 1 0 422261153 41295872 8782 4294967295 134512640 134672761 3221224560 3221223056 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10082 8782 603 41 0 10041 0
vsize: 40328
[startup+120.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9359 0 0 0 11953 42 0 0 25 0 1 0 422261153 41295872 8783 4294967295 134512640 134672761 3221224560 3221223152 134607908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10082 8783 603 41 0 10041 0
vsize: 40328
[startup+130.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9361 0 0 0 12952 43 0 0 25 0 1 0 422261153 41295872 8785 4294967295 134512640 134672761 3221224560 3221223008 134644038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10082 8785 603 41 0 10041 0
vsize: 40328
[startup+140.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9363 0 0 0 13952 43 0 0 25 0 1 0 422261153 41295872 8787 4294967295 134512640 134672761 3221224560 3221223056 134644272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10082 8787 603 41 0 10041 0
vsize: 40328
[startup+150.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9366 0 0 0 14951 44 0 0 25 0 1 0 422261153 41295872 8790 4294967295 134512640 134672761 3221224560 3221223056 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10082 8790 603 41 0 10041 0
vsize: 40328
[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9369 0 0 0 15951 44 0 0 25 0 1 0 422261153 41295872 8793 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10082 8793 603 41 0 10041 0
vsize: 40328
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9371 0 0 0 16951 44 0 0 25 0 1 0 422261153 41295872 8795 4294967295 134512640 134672761 3221224560 3221223088 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10082 8795 603 41 0 10041 0
vsize: 40328
[startup+180.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9374 0 0 0 17951 44 0 0 25 0 1 0 422261153 41295872 8798 4294967295 134512640 134672761 3221224560 3221222992 134605852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10082 8798 603 41 0 10041 0
vsize: 40328
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9397 0 0 0 18951 44 0 0 25 0 1 0 422261153 41304064 8775 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10084 8775 603 41 0 10043 0
vsize: 40336
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9397 0 0 0 19951 44 0 0 25 0 1 0 422261153 41304064 8775 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10084 8775 603 41 0 10043 0
vsize: 40336
[startup+210.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9711 0 0 0 20951 45 0 0 25 0 1 0 422261153 42348544 9043 4294967295 134512640 134672761 3221224560 3221222784 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10339 9043 603 41 0 10298 0
vsize: 41356
[startup+220.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9711 0 0 0 21952 45 0 0 25 0 1 0 422261153 42348544 9043 4294967295 134512640 134672761 3221224560 3221223052 134642955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10339 9043 603 41 0 10298 0
vsize: 41356
[startup+230.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9711 0 0 0 22952 45 0 0 25 0 1 0 422261153 42348544 9043 4294967295 134512640 134672761 3221224560 3221223104 134621095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10339 9043 603 41 0 10298 0
vsize: 41356
[startup+240.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9711 0 0 0 23952 45 0 0 25 0 1 0 422261153 40910848 8738 4294967295 134512640 134672761 3221224560 3221223008 134643774 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9988 8738 603 41 0 9947 0
vsize: 39952
[startup+250.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 9711 0 0 0 24952 45 0 0 25 0 1 0 422261153 40910848 8738 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9988 8738 603 41 0 9947 0
vsize: 39952
[startup+260.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 10053 0 0 0 25952 46 0 0 25 0 1 0 422261153 42328064 9080 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10334 9080 603 41 0 10293 0
vsize: 41336
[startup+270.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 10857 0 0 0 26950 48 0 0 25 0 1 0 422261153 45563904 9884 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11124 9884 603 41 0 11083 0
vsize: 44496
[startup+280.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 11611 0 0 0 27948 50 0 0 25 0 1 0 422261153 48750592 10638 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11902 10638 603 41 0 11861 0
vsize: 47608
[startup+290.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 12465 0 0 0 28946 52 0 0 25 0 1 0 422261153 52281344 11492 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12764 11492 603 41 0 12723 0
vsize: 51056
[startup+300.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 13436 0 0 0 29944 54 0 0 25 0 1 0 422261153 56143872 12463 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 12463 603 41 0 13666 0
vsize: 54828
[startup+310.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 14296 0 0 0 30942 55 0 0 25 0 1 0 422261153 59789312 13323 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14597 13323 603 41 0 14556 0
vsize: 58388
[startup+320.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 14743 0 0 0 31942 56 0 0 25 0 1 0 422261153 61620224 13770 4294967295 134512640 134672761 3221224560 3221223704 134616371 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15044 13770 603 41 0 15003 0
vsize: 60176
[startup+330.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 15685 0 0 0 32940 58 0 0 25 0 1 0 422261153 65490944 14712 4294967295 134512640 134672761 3221224560 3221223496 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15989 14712 603 41 0 15948 0
vsize: 63956
[startup+340.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 17666 0 0 0 33932 66 0 0 25 0 1 0 422261153 75350016 16693 4294967295 134512640 134672761 3221224560 3221222820 1075346926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18396 16693 603 41 0 18355 0
vsize: 73584
[startup+350.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 18309 0 0 0 34926 72 0 0 25 0 1 0 422261153 69992448 15744 4294967295 134512640 134672761 3221224560 3221222980 134644220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17088 15744 603 41 0 17047 0
vsize: 68352
[startup+360.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 18309 0 0 0 35908 89 0 0 25 0 1 0 422261153 69992448 15744 4294967295 134512640 134672761 3221224560 3221223008 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17088 15744 603 41 0 17047 0
vsize: 68352
[startup+370.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 18309 0 0 0 36908 89 0 0 25 0 1 0 422261153 69992448 15744 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17088 15744 603 41 0 17047 0
vsize: 68352
[startup+380.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 18310 0 0 0 37907 90 0 0 25 0 1 0 422261153 69992448 15745 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17088 15745 603 41 0 17047 0
vsize: 68352
[startup+390.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 18311 0 0 0 38907 90 0 0 25 0 1 0 422261153 69992448 15746 4294967295 134512640 134672761 3221224560 3221223704 134616108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17088 15746 603 41 0 17047 0
vsize: 68352
[startup+400.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 18313 0 0 0 39907 90 0 0 25 0 1 0 422261153 69992448 15748 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17088 15748 603 41 0 17047 0
vsize: 68352
[startup+410.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 18434 0 0 0 40907 90 0 0 25 0 1 0 422261153 70520832 15869 4294967295 134512640 134672761 3221224560 3221223684 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17217 15869 603 41 0 17176 0
vsize: 68868
[startup+420.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 19351 0 0 0 41906 92 0 0 25 0 1 0 422261153 74260480 16786 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18130 16786 603 41 0 18089 0
vsize: 72520
[startup+430.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 20008 0 0 0 42905 93 0 0 25 0 1 0 422261153 77152256 17443 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18836 17443 603 41 0 18795 0
vsize: 75344
[startup+440.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 20672 0 0 0 43904 94 0 0 25 0 1 0 422261153 79867904 18107 4294967295 134512640 134672761 3221224560 3221223704 134616296 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19499 18107 603 41 0 19458 0
vsize: 77996
[startup+450.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 21238 0 0 0 44902 96 0 0 25 0 1 0 422261153 82173952 18673 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20062 18673 603 41 0 20021 0
vsize: 80248
[startup+460.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 21786 0 0 0 45901 97 0 0 25 0 1 0 422261153 84361216 19221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20596 19221 603 41 0 20555 0
vsize: 82384
[startup+470.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 22562 0 0 0 46899 99 0 0 25 0 1 0 422261153 87592960 19997 4294967295 134512640 134672761 3221224560 3221223232 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21385 19997 603 41 0 21344 0
vsize: 85540
[startup+480.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25121 0 0 0 47886 113 0 0 25 0 1 0 422261153 92274688 21150 4294967295 134512640 134672761 3221224560 3221223104 134621081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22528 21150 603 41 0 22487 0
vsize: 90112
[startup+490.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25169 0 0 0 48882 117 0 0 25 0 1 0 422261153 89907200 20860 4294967295 134512640 134672761 3221224560 3221223008 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21950 20860 603 41 0 21909 0
vsize: 87800
[startup+500.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25169 0 0 0 49799 174 0 0 25 0 1 0 422261153 89907200 20860 4294967295 134512640 134672761 3221224560 3221223008 134643518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21950 20860 603 41 0 21909 0
vsize: 87800
[startup+510.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25169 0 0 0 50799 174 0 0 25 0 1 0 422261153 89907200 20860 4294967295 134512640 134672761 3221224560 3221223008 134643468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21950 20860 603 41 0 21909 0
vsize: 87800
[startup+520.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25169 0 0 0 51798 174 0 0 25 0 1 0 422261153 89907200 20860 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21950 20860 603 41 0 21909 0
vsize: 87800
[startup+530.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25459 0 0 0 52798 175 0 0 25 0 1 0 422261153 92192768 21150 4294967295 134512640 134672761 3221224560 3221222960 134604081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22508 21150 603 41 0 22467 0
vsize: 90032
[startup+540.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25459 0 0 0 53798 175 0 0 25 0 1 0 422261153 89907200 20860 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21950 20860 603 41 0 21909 0
vsize: 87800
[startup+550.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25459 0 0 0 54798 175 0 0 25 0 1 0 422261153 89907200 20860 4294967295 134512640 134672761 3221224560 3221223816 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21950 20860 603 41 0 21909 0
vsize: 87800
[startup+560.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 25851 0 0 0 55798 176 0 0 25 0 1 0 422261153 91521024 21252 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22344 21252 603 41 0 22303 0
vsize: 89376
[startup+570.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 26789 0 0 0 56795 178 0 0 25 0 1 0 422261153 95379456 22190 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23286 22190 603 41 0 23245 0
vsize: 93144
[startup+580.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 27507 0 0 0 57794 180 0 0 25 0 1 0 422261153 98406400 22908 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24025 22908 603 41 0 23984 0
vsize: 96100
[startup+590.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 28426 0 0 0 58792 182 0 0 25 0 1 0 422261153 102117376 23827 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24931 23827 603 41 0 24890 0
vsize: 99724
[startup+600.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 29499 0 0 0 59789 185 0 0 25 0 1 0 422261153 106434560 24900 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25985 24900 603 41 0 25944 0
vsize: 103940
[startup+610.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 30293 0 0 0 60788 186 0 0 25 0 1 0 422261153 109670400 25694 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26775 25694 603 41 0 26734 0
vsize: 107100
[startup+620.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 30827 0 0 0 61787 188 0 0 25 0 1 0 422261153 111927296 26228 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27326 26228 603 41 0 27285 0
vsize: 109304
[startup+630.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 31232 0 0 0 62786 189 0 0 25 0 1 0 422261153 113508352 26633 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27712 26633 603 41 0 27671 0
vsize: 110848
[startup+640.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 32192 0 0 0 63784 191 0 0 25 0 1 0 422261153 117547008 27593 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28698 27593 603 41 0 28657 0
vsize: 114792
[startup+650.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 32492 0 0 0 64783 192 0 0 25 0 1 0 422261153 118693888 27893 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28978 27893 603 41 0 28937 0
vsize: 115912
[startup+660.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 32911 0 0 0 65782 193 0 0 25 0 1 0 422261153 120369152 28312 4294967295 134512640 134672761 3221224560 3221223744 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29387 28312 603 41 0 29346 0
vsize: 117548
[startup+670.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 33364 0 0 0 66781 194 0 0 25 0 1 0 422261153 122290176 28765 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 28765 603 41 0 29815 0
vsize: 119424
[startup+680.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36240 0 0 0 67757 218 0 0 25 0 1 0 422261153 131534848 29552 4294967295 134512640 134672761 3221224560 3221223052 134642754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32113 29552 603 41 0 32072 0
vsize: 128452
[startup+690.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36240 0 0 0 68749 225 0 0 25 0 1 0 422261153 129658880 29262 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31655 29262 603 41 0 31614 0
vsize: 126620
[startup+700.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 69749 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+710.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 70749 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+720.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 71748 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223232 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+730.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 72748 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+740.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 73748 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+750.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 74749 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223600 134614268 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+760.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 75749 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+770.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 76749 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+780.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 77749 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+790.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36310 0 0 0 78749 225 0 0 25 0 1 0 422261153 129921024 29332 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29332 603 41 0 31678 0
vsize: 126876
[startup+800.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 79749 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+810.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 80750 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+820.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 81750 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223504 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+830.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 82750 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223704 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+840.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 83750 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+850.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 84750 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+860.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 85751 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+870.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 86751 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223704 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+880.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 87751 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+890.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 88751 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+900.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 89751 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+910.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 90752 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+920.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 91752 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+930.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36311 0 0 0 92752 225 0 0 25 0 1 0 422261153 129921024 29333 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 29333 603 41 0 31678 0
vsize: 126876
[startup+940.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 36628 0 0 0 93751 226 0 0 25 0 1 0 422261153 131244032 29650 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32042 29650 603 41 0 32001 0
vsize: 128168
[startup+950.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 37019 0 0 0 94751 227 0 0 25 0 1 0 422261153 132927488 30041 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32453 30041 603 41 0 32412 0
vsize: 129812
[startup+960.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 37390 0 0 0 95750 228 0 0 25 0 1 0 422261153 134352896 30412 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32801 30412 603 41 0 32760 0
vsize: 131204
[startup+970.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 37869 0 0 0 96749 229 0 0 25 0 1 0 422261153 136318976 30891 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33281 30891 603 41 0 33240 0
vsize: 133124
[startup+980.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 38310 0 0 0 97748 231 0 0 25 0 1 0 422261153 138137600 31332 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33725 31332 603 41 0 33684 0
vsize: 134900
[startup+990.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 39013 0 0 0 98746 232 0 0 25 0 1 0 422261153 141246464 32035 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34484 32035 603 41 0 34443 0
vsize: 137936
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 39426 0 0 0 99745 233 0 0 25 0 1 0 422261153 142987264 32448 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34909 32448 603 41 0 34868 0
vsize: 139636
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 39790 0 0 0 100744 234 0 0 25 0 1 0 422261153 144498688 32812 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35278 32812 603 41 0 35237 0
vsize: 141112
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 40273 0 0 0 101744 235 0 0 25 0 1 0 422261153 146448384 33295 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35754 33295 603 41 0 35713 0
vsize: 143016
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 40480 0 0 0 102743 236 0 0 25 0 1 0 422261153 147316736 33502 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35966 33502 603 41 0 35925 0
vsize: 143864
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 40986 0 0 0 103743 237 0 0 25 0 1 0 422261153 149401600 34008 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36475 34008 603 41 0 36434 0
vsize: 145900
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 41430 0 0 0 104741 238 0 0 25 0 1 0 422261153 151093248 34452 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36888 34452 603 41 0 36847 0
vsize: 147552
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 42168 0 0 0 105739 241 0 0 25 0 1 0 422261153 154193920 35190 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37645 35190 603 41 0 37604 0
vsize: 150580
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 42922 0 0 0 106737 243 0 0 25 0 1 0 422261153 157319168 35944 4294967295 134512640 134672761 3221224560 3221223704 134616320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38408 35944 603 41 0 38367 0
vsize: 153632
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 43186 0 0 0 107736 244 0 0 25 0 1 0 422261153 158351360 36208 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38660 36208 603 41 0 38619 0
vsize: 154640
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 43800 0 0 0 108735 245 0 0 25 0 1 0 422261153 160833536 36822 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39266 36822 603 41 0 39225 0
vsize: 157064
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 44203 0 0 0 109734 246 0 0 25 0 1 0 422261153 162516992 37225 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39677 37225 603 41 0 39636 0
vsize: 158708
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 44529 0 0 0 110734 247 0 0 25 0 1 0 422261153 163803136 37551 4294967295 134512640 134672761 3221224560 3221223704 134616126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39991 37551 603 41 0 39950 0
vsize: 159964
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 44735 0 0 0 111733 248 0 0 25 0 1 0 422261153 164724736 37757 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40216 37757 603 41 0 40175 0
vsize: 160864
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 45293 0 0 0 112731 250 0 0 25 0 1 0 422261153 166903808 38315 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40748 38315 603 41 0 40707 0
vsize: 162992
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 45705 0 0 0 113730 251 0 0 25 0 1 0 422261153 168574976 38727 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41156 38727 603 41 0 41115 0
vsize: 164624
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 46339 0 0 0 114729 253 0 0 25 0 1 0 422261153 171208704 39361 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41799 39361 603 41 0 41758 0
vsize: 167196
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 46622 0 0 0 115729 253 0 0 25 0 1 0 422261153 172363776 39644 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42081 39644 603 41 0 42040 0
vsize: 168324
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 46981 0 0 0 116727 255 0 0 25 0 1 0 422261153 173826048 40003 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42438 40003 603 41 0 42397 0
vsize: 169752
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 47350 0 0 0 117726 256 0 0 25 0 1 0 422261153 175296512 40372 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42797 40372 603 41 0 42756 0
vsize: 171188
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 47928 0 0 0 118725 257 0 0 25 0 1 0 422261153 177774592 40950 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43402 40950 603 41 0 43361 0
vsize: 173608
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 48158 0 0 0 119725 258 0 0 25 0 1 0 422261153 178708480 41180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43630 41180 603 41 0 43589 0
vsize: 174520
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6096
Raw data (stat): 6094 (minisat+) R 6093 32461 32460 0 -1 0 48473 0 0 0 120724 259 0 0 25 0 1 0 422261153 179974144 41495 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43939 41495 603 41 0 43898 0
vsize: 175756
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.19 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 6096
Raw data (stat): 6094 (minisat+) Z 6093 32461 32460 0 -1 12 48474 0 0 0 120724 272 0 0 25 0 1 0 422261153 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.19
CPU time (s): 1209.97
CPU user time (s): 1207.25
CPU system time (s): 2.72358
CPU usage (%): 99.9824
Max. virtual memory (Kb): 175756
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####