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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        895856 kB
Buffers:         37696 kB
Cached:          81100 kB
SwapCached:          0 kB
Active:          74488 kB
Inactive:        47176 kB
HighTotal:      131008 kB
HighFree:        46116 kB
LowTotal:       903652 kB
LowFree:        849740 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11524 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:24:08 (client local time) WITH STATUS 10 IN 1209.81 SECONDS
stats: 4098 7 1209.81 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80035 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 |   80035   160070 |   24010       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   80035   160070 |   32014       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.17237 s)
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  147951   319392 |   44385       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/46228          
c   -- var.elim.:  2000/46228          
c   -- var.elim.:  3000/46228          
c   -- var.elim.:  4000/46228          
c   -- var.elim.:  5000/46228          
c   -- var.elim.:  6000/46228          
c   -- var.elim.:  7000/46228          
c   -- var.elim.:  8000/46228          
c   -- var.elim.:  9000/46228          
c   -- var.elim.:  10000/46228          
c   -- var.elim.:  11000/46228          
c   -- var.elim.:  12000/46228          
c   -- var.elim.:  13000/46228          
c   -- var.elim.:  14000/46228          
c   -- var.elim.:  15000/46228          
c   -- var.elim.:  16000/46228          
c   -- var.elim.:  17000/46228          
c   -- var.elim.:  18000/46228          
c   -- var.elim.:  19000/46228          
c   -- var.elim.:  20000/46228          
c   -- var.elim.:  21000/46228          
c   -- var.elim.:  22000/46228          
c   -- var.elim.:  23000/46228          
c   -- var.elim.:  24000/46228          
c   -- var.elim.:  25000/46228          
c   -- var.elim.:  26000/46228          
c   -- var.elim.:  27000/46228          
c   -- var.elim.:  28000/46228          
c   -- var.elim.:  29000/46228          
c   -- var.elim.:  30000/46228          
c   -- var.elim.:  31000/46228          
c   -- var.elim.:  32000/46228          
c   -- var.elim.:  33000/46228          
c   -- var.elim.:  34000/46228          
c   -- var.elim.:  35000/46228          
c   -- var.elim.:  36000/46228          
c   -- var.elim.:  37000/46228          
c   -- var.elim.:  38000/46228          
c   -- var.elim.:  39000/46228          
c   -- var.elim.:  40000/46228          
c   -- var.elim.:  41000/46228          
c   -- var.elim.:  42000/46228          
c   -- var.elim.:  43000/46228          
c   -- var.elim.:  44000/46228          
c   -- var.elim.:  45000/46228          
c   -- var.elim.:  46000/46228          
c   -- var.elim.:  46228/46228          
c   -- var.elim.:  1000/23434          
c   -- var.elim.:  2000/23434          
c   -- var.elim.:  3000/23434          
c   -- var.elim.:  4000/23434          
c   -- var.elim.:  5000/23434          
c   -- var.elim.:  6000/23434          
c   -- var.elim.:  7000/23434          
c   -- var.elim.:  8000/23434          
c   -- var.elim.:  9000/23434          
c   -- var.elim.:  10000/23434          
c   -- var.elim.:  11000/23434          
c   -- var.elim.:  12000/23434          
c   -- var.elim.:  13000/23434          
c   -- var.elim.:  14000/23434          
c   -- var.elim.:  15000/23434          
c   -- var.elim.:  16000/23434          
c   -- var.elim.:  17000/23434          
c   -- var.elim.:  18000/23434          
c   -- var.elim.:  19000/23434          
c   -- var.elim.:  20000/23434          
c   -- var.elim.:  21000/23434          
c   -- var.elim.:  22000/23434          
c   -- var.elim.:  23000/23434          
c   -- var.elim.:  23434/23434          
c   -- var.elim.:  197/197          
c   -- var.elim.:  101/101          
c   -- subsuming                       
c   -- var.elim.:  1000/9288          
c   -- var.elim.:  2000/9288          
c   -- var.elim.:  3000/9288          
c   -- var.elim.:  4000/9288          
c   -- var.elim.:  5000/9288          
c   -- var.elim.:  6000/9288          
c   -- var.elim.:  7000/9288          
c   -- var.elim.:  8000/9288          
c   -- var.elim.:  9000/9288          
c   -- var.elim.:  9288/9288          
c   -- var.elim.:  463/463          
c   -- subsuming                       
c   -- var.elim.:  37/37          
c |         0 |   99979   340428 |      --       0       --      -- |     --   | -47972/21037
c |         0 |   99979   340428 |   39991       0        0     nan |  0.000 % |
c |       100 |   99979   340428 |   43990     100    21718   217.2 | 53.551 % |
c |       251 |   99911   339774 |   48356     248    42079   169.7 | 53.680 % |
c |       477 |   99911   339774 |   53192     474    86261   182.0 | 53.680 % |
c |       814 |   99911   339774 |   58511     811   154127   190.0 | 53.680 % |
c |      1321 |   99911   339774 |   64363    1318   262184   198.9 | 53.680 % |
c |      2080 |   99856   339234 |   70760    2072   393910   190.1 | 53.778 % |
c |      3219 |   99824   338922 |   77811    3206   615824   192.1 | 53.847 % |
c |      4927 |   99635   337041 |   85430    4901   958804   195.6 | 54.240 % |
c |      7489 |   99275   333651 |   93634    7443  1543775   207.4 | 54.968 % |
c |     11333 |   99183   332746 |  102902   11262  2544715   226.0 | 55.165 % |
c |     17101 |   98494   325505 |  112405   16958  4080575   240.6 | 56.509 % |
c |     25750 |   97650   317543 |  122587   25479  6768090   265.6 | 58.312 % |
c ==============================================================================
c (current CPU-time: 398.227 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 |     34358 |  107061   338492 |   32118   33955  9552886   281.3 | 58.312 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19306          
c   -- var.elim.:  2000/19306          
c   -- var.elim.:  3000/19306          
c   -- var.elim.:  4000/19306          
c   -- var.elim.:  5000/19306          
c   -- var.elim.:  6000/19306          
c   -- var.elim.:  7000/19306          
c   -- var.elim.:  8000/19306          
c   -- var.elim.:  9000/19306          
c   -- var.elim.:  10000/19306          
c   -- var.elim.:  11000/19306          
c   -- var.elim.:  12000/19306          
c   -- var.elim.:  13000/19306          
c   -- var.elim.:  14000/19306          
c   -- var.elim.:  15000/19306          
c   -- var.elim.:  16000/19306          
c   -- var.elim.:  17000/19306          
c   -- var.elim.:  18000/19306          
c   -- var.elim.:  19000/19306          
c   -- var.elim.:  19306/19306          
c   -- var.elim.:  1000/7416          
c   -- var.elim.:  2000/7416          
c   -- var.elim.:  3000/7416          
c   -- var.elim.:  4000/7416          
c   -- var.elim.:  5000/7416          
c   -- var.elim.:  6000/7416          
c   -- var.elim.:  7000/7416          
c   -- var.elim.:  7416/7416          
c   -- var.elim.:  516/516          
c   -- subsuming                       
c   -- var.elim.:  1000/6157          
c   -- var.elim.:  2000/6157          
c   -- var.elim.:  3000/6157          
c   -- var.elim.:  4000/6157          
c   -- var.elim.:  5000/6157          
c   -- var.elim.:  6000/6157          
c   -- var.elim.:  6157/6157          
c   -- var.elim.:  172/172          
c |     34358 |   97087   322410 |      --   33955       --      -- |     --   | -9966/-16065
c |     34358 |   97087   322410 |   38834   33955  9552886   281.3 | 58.312 % |
c |     34458 |   97087   322410 |   42718   34055  9577763   281.2 | 67.590 % |
c |     34608 |   97055   322095 |   46974   34204  9603042   280.8 | 67.645 % |
c |     34833 |   97053   322072 |   51671   34047  9538989   280.2 | 67.648 % |
c |     35170 |   96845   320057 |   56716   34369  9617004   279.8 | 67.996 % |
c |     35676 |   96739   319035 |   62319   34829  9738362   279.6 | 68.179 % |
c |     36436 |   96707   318714 |   68528   35585  9950250   279.6 | 68.233 % |
c |     37575 |   96645   318116 |   75333   36717 10284263   280.1 | 68.340 % |
c |     39283 |   96421   315825 |   82674   38321 10850931   283.2 | 68.715 % |
c |     41845 |   96273   314376 |   90802   40853 11648168   285.1 | 68.966 % |
c |     45690 |   96024   311860 |   99624   44636 12926992   289.6 | 69.379 % |
c |     51456 |   95464   306414 |  108947   50234 14780580   294.2 | 70.305 % |
c |     60105 |   95075   302666 |  119354   58789 17901048   304.5 | 70.959 % |
c |     73079 |   93927   291067 |  129704   71449 22486115   314.7 | 72.893 % |
c |     92540 |   93018   282205 |  141294   90647 29433011   324.7 | 74.424 % |
c |    121732 |   91629   268307 |  153102  119128 40555554   340.4 | 76.753 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C4#### 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.85 0.95 0.90 2/54 27173
Raw data (stat): 27173 (runsolver) R 27172 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422268291 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 27173
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9293 0 0 0 956 41 0 0 25 0 1 0 422268291 40280064 8717 4294967295 134512640 134672761 3221224560 3221221776 134566692 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9834 8717 603 41 0 9793 0
vsize: 39336
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 27173
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9299 0 0 0 1955 42 0 0 25 0 1 0 422268291 40280064 8723 4294967295 134512640 134672761 3221224560 3221222984 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 8723 603 41 0 9793 0
vsize: 39336
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 27173
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9300 0 0 0 2955 43 0 0 25 0 1 0 422268291 40280064 8724 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 8724 603 41 0 9793 0
vsize: 39336
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 27173
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9301 0 0 0 3955 43 0 0 25 0 1 0 422268291 40280064 8725 4294967295 134512640 134672761 3221224560 3221223056 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 8725 603 41 0 9793 0
vsize: 39336
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 27173
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9302 0 0 0 4955 43 0 0 25 0 1 0 422268291 40280064 8726 4294967295 134512640 134672761 3221224560 3221222244 134566652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 8726 603 41 0 9793 0
vsize: 39336
[startup+60.0008 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 27173
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9303 0 0 0 5955 43 0 0 25 0 1 0 422268291 40280064 8727 4294967295 134512640 134672761 3221224560 3221223008 134643574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 8727 603 41 0 9793 0
vsize: 39336
[startup+70.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 27173
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9310 0 0 0 6955 43 0 0 25 0 1 0 422268291 40280064 8734 4294967295 134512640 134672761 3221224560 3221222992 134605852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 8734 603 41 0 9793 0
vsize: 39336
[startup+80.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27173
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9311 0 0 0 7955 43 0 0 25 0 1 0 422268291 40280064 8735 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 8735 603 41 0 9793 0
vsize: 39336
[startup+90.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9317 0 0 0 8956 43 0 0 25 0 1 0 422268291 40411136 8741 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9866 8741 603 41 0 9825 0
vsize: 39464
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9350 0 0 0 9956 43 0 0 25 0 1 0 422268291 40673280 8774 4294967295 134512640 134672761 3221224560 3221222816 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9930 8774 603 41 0 9889 0
vsize: 39720
[startup+110.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9351 0 0 0 10956 43 0 0 25 0 1 0 422268291 40673280 8775 4294967295 134512640 134672761 3221224560 3221221952 134566724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9930 8775 603 41 0 9889 0
vsize: 39720
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9353 0 0 0 11956 43 0 0 25 0 1 0 422268291 40673280 8777 4294967295 134512640 134672761 3221224560 3221222112 134566484 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9930 8777 603 41 0 9889 0
vsize: 39720
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9355 0 0 0 12956 43 0 0 25 0 1 0 422268291 40673280 8779 4294967295 134512640 134672761 3221224560 3221222352 134566562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9930 8779 603 41 0 9889 0
vsize: 39720
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9358 0 0 0 13956 43 0 0 25 0 1 0 422268291 40673280 8782 4294967295 134512640 134672761 3221224560 3221222984 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9930 8782 603 41 0 9889 0
vsize: 39720
[startup+150.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9359 0 0 0 14957 43 0 0 25 0 1 0 422268291 40673280 8783 4294967295 134512640 134672761 3221224560 3221222840 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9930 8783 603 41 0 9889 0
vsize: 39720
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9362 0 0 0 15957 43 0 0 25 0 1 0 422268291 40673280 8786 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9930 8786 603 41 0 9889 0
vsize: 39720
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9365 0 0 0 16957 43 0 0 25 0 1 0 422268291 40673280 8789 4294967295 134512640 134672761 3221224560 3221223088 134606949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9930 8789 603 41 0 9889 0
vsize: 39720
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9375 0 0 0 17957 43 0 0 25 0 1 0 422268291 40484864 8753 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9884 8753 603 41 0 9843 0
vsize: 39536
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9375 0 0 0 18957 43 0 0 25 0 1 0 422268291 40484864 8753 4294967295 134512640 134672761 3221224560 3221223008 134643636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9884 8753 603 41 0 9843 0
vsize: 39536
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9625 0 0 0 19957 43 0 0 25 0 1 0 422268291 41246720 8957 4294967295 134512640 134672761 3221224560 3221223272 134643292 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10070 8957 603 41 0 10029 0
vsize: 40280
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9702 0 0 0 20957 44 0 0 25 0 1 0 422268291 42467328 9034 4294967295 134512640 134672761 3221224560 3221222192 134566687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10368 9034 603 41 0 10327 0
vsize: 41472
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9702 0 0 0 21957 44 0 0 25 0 1 0 422268291 42467328 9034 4294967295 134512640 134672761 3221224560 3221222732 134642759 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10368 9034 603 41 0 10327 0
vsize: 41472
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9702 0 0 0 22957 44 0 0 25 0 1 0 422268291 42467328 9034 4294967295 134512640 134672761 3221224560 3221223104 134621179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10368 9034 603 41 0 10327 0
vsize: 41472
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9702 0 0 0 23957 44 0 0 25 0 1 0 422268291 42467328 9034 4294967295 134512640 134672761 3221224560 3221223104 134621227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10368 9034 603 41 0 10327 0
vsize: 41472
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 9702 0 0 0 24957 44 0 0 25 0 1 0 422268291 40288256 8730 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9836 8730 603 41 0 9795 0
vsize: 39344
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 10106 0 0 0 25957 45 0 0 25 0 1 0 422268291 40820736 8844 4294967295 134512640 134672761 3221224560 3221223728 134564736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9966 8844 603 41 0 9925 0
vsize: 39864
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 10665 0 0 0 26956 46 0 0 25 0 1 0 422268291 43048960 9403 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10510 9403 603 41 0 10469 0
vsize: 42040
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 11343 0 0 0 27954 47 0 0 25 0 1 0 422268291 45899776 10081 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11206 10081 603 41 0 11165 0
vsize: 44824
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 12168 0 0 0 28952 50 0 0 25 0 1 0 422268291 49246208 10906 4294967295 134512640 134672761 3221224560 3221223696 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12023 10906 603 41 0 11982 0
vsize: 48092
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 12741 0 0 0 29951 51 0 0 25 0 1 0 422268291 51564544 11479 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12589 11479 603 41 0 12548 0
vsize: 50356
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 13342 0 0 0 30949 52 0 0 25 0 1 0 422268291 54030336 12080 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13191 12080 603 41 0 13150 0
vsize: 52764
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 14112 0 0 0 31948 54 0 0 25 0 1 0 422268291 57278464 12850 4294967295 134512640 134672761 3221224560 3221223704 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13984 12850 603 41 0 13943 0
vsize: 55936
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 14794 0 0 0 32946 55 0 0 25 0 1 0 422268291 60035072 13532 4294967295 134512640 134672761 3221224560 3221223744 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14657 13532 603 41 0 14616 0
vsize: 58628
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 15534 0 0 0 33945 57 0 0 25 0 1 0 422268291 63041536 14272 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15391 14272 603 41 0 15350 0
vsize: 61564
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 16227 0 0 0 34944 58 0 0 25 0 1 0 422268291 65826816 14965 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16071 14965 603 41 0 16030 0
vsize: 64284
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 16746 0 0 0 35943 59 0 0 25 0 1 0 422268291 68030464 15484 4294967295 134512640 134672761 3221224560 3221223472 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16609 15484 603 41 0 16568 0
vsize: 66436
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 17469 0 0 0 36941 61 0 0 25 0 1 0 422268291 70995968 16207 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17333 16207 603 41 0 17292 0
vsize: 69332
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 18119 0 0 0 37940 62 0 0 25 0 1 0 422268291 73576448 16857 4294967295 134512640 134672761 3221224560 3221223704 134616108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17963 16857 603 41 0 17922 0
vsize: 71852
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 18627 0 0 0 38939 64 0 0 25 0 1 0 422268291 75608064 17365 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18459 17365 603 41 0 18418 0
vsize: 73836
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21345 0 0 0 39928 74 0 0 25 0 1 0 422268291 82825216 18957 4294967295 134512640 134672761 3221224560 3221223104 134621041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20221 18957 603 41 0 20180 0
vsize: 80884
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21345 0 0 0 40917 85 0 0 25 0 1 0 422268291 80637952 18667 4294967295 134512640 134672761 3221224560 3221223008 134606977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19687 18667 603 41 0 19646 0
vsize: 78748
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21345 0 0 0 41816 135 0 0 25 0 1 0 422268291 80637952 18667 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19687 18667 603 41 0 19646 0
vsize: 78748
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21345 0 0 0 42816 135 0 0 25 0 1 0 422268291 80637952 18667 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19687 18667 603 41 0 19646 0
vsize: 78748
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21345 0 0 0 43816 135 0 0 25 0 1 0 422268291 80637952 18667 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19687 18667 603 41 0 19646 0
vsize: 78748
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21635 0 0 0 44816 135 0 0 25 0 1 0 422268291 82964480 18957 4294967295 134512640 134672761 3221224560 3221223024 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20255 18957 603 41 0 20214 0
vsize: 81020
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21635 0 0 0 45816 135 0 0 25 0 1 0 422268291 80637952 18667 4294967295 134512640 134672761 3221224560 3221223008 134643468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19687 18667 603 41 0 19646 0
vsize: 78748
[startup+470 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21635 0 0 0 46816 135 0 0 25 0 1 0 422268291 80637952 18667 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19687 18667 603 41 0 19646 0
vsize: 78748
[startup+480 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 21638 0 0 0 47816 135 0 0 25 0 1 0 422268291 80756736 18670 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19716 18670 603 41 0 19675 0
vsize: 78864
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 22249 0 0 0 48815 137 0 0 25 0 1 0 422268291 83214336 19281 4294967295 134512640 134672761 3221224560 3221222400 134566712 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20316 19281 603 41 0 20275 0
vsize: 81264
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 22714 0 0 0 49815 137 0 0 25 0 1 0 422268291 85131264 19746 4294967295 134512640 134672761 3221224560 3221223704 134616339 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20784 19746 603 41 0 20743 0
vsize: 83136
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 23244 0 0 0 50814 139 0 0 25 0 1 0 422268291 87199744 20276 4294967295 134512640 134672761 3221224560 3221223600 134614205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21289 20276 603 41 0 21248 0
vsize: 85156
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 23888 0 0 0 51812 140 0 0 25 0 1 0 422268291 89931776 20920 4294967295 134512640 134672761 3221224560 3221223704 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21956 20920 603 41 0 21915 0
vsize: 87824
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 24453 0 0 0 52812 141 0 0 25 0 1 0 422268291 92258304 21485 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22524 21485 603 41 0 22483 0
vsize: 90096
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 24841 0 0 0 53811 142 0 0 25 0 1 0 422268291 93814784 21873 4294967295 134512640 134672761 3221224560 3221223552 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22904 21873 603 41 0 22863 0
vsize: 91616
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 25270 0 0 0 54810 143 0 0 25 0 1 0 422268291 95498240 22302 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23315 22302 603 41 0 23274 0
vsize: 93260
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 25764 0 0 0 55809 144 0 0 25 0 1 0 422268291 97574912 22796 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23822 22796 603 41 0 23781 0
vsize: 95288
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 26450 0 0 0 56808 146 0 0 25 0 1 0 422268291 100302848 23482 4294967295 134512640 134672761 3221224560 3221223704 134616373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24488 23482 603 41 0 24447 0
vsize: 97952
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 27138 0 0 0 57807 147 0 0 25 0 1 0 422268291 103170048 24170 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25188 24170 603 41 0 25147 0
vsize: 100752
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 27643 0 0 0 58805 149 0 0 25 0 1 0 422268291 105226240 24675 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25690 24675 603 41 0 25649 0
vsize: 102760
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 28172 0 0 0 59804 150 0 0 25 0 1 0 422268291 107442176 25204 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26231 25204 603 41 0 26190 0
vsize: 104924
[startup+610.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 28641 0 0 0 60803 151 0 0 25 0 1 0 422268291 109350912 25673 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26697 25673 603 41 0 26656 0
vsize: 106788
[startup+620.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 29073 0 0 0 61802 152 0 0 25 0 1 0 422268291 111046656 26105 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27111 26105 603 41 0 27070 0
vsize: 108444
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 29731 0 0 0 62801 154 0 0 25 0 1 0 422268291 113778688 26763 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27778 26763 603 41 0 27737 0
vsize: 111112
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 30079 0 0 0 63800 155 0 0 25 0 1 0 422268291 115204096 27111 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28126 27111 603 41 0 28085 0
vsize: 112504
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 30663 0 0 0 64799 156 0 0 25 0 1 0 422268291 117518336 27695 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28691 27695 603 41 0 28650 0
vsize: 114764
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 31378 0 0 0 65798 158 0 0 25 0 1 0 422268291 120520704 28410 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29424 28410 603 41 0 29383 0
vsize: 117696
[startup+670.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 31980 0 0 0 66797 158 0 0 25 0 1 0 422268291 123006976 29012 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30031 29012 603 41 0 29990 0
vsize: 120124
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 32361 0 0 0 67797 159 0 0 25 0 1 0 422268291 124735488 29393 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30453 29393 603 41 0 30412 0
vsize: 121812
[startup+690.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 32662 0 0 0 68796 160 0 0 25 0 1 0 422268291 126033920 29694 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30770 29694 603 41 0 30729 0
vsize: 123080
[startup+700.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 33000 0 0 0 69796 160 0 0 25 0 1 0 422268291 127320064 30032 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31084 30032 603 41 0 31043 0
vsize: 124336
[startup+710.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 33440 0 0 0 70795 161 0 0 25 0 1 0 422268291 129167360 30472 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31535 30472 603 41 0 31494 0
vsize: 126140
[startup+720.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 33844 0 0 0 71794 162 0 0 25 0 1 0 422268291 130813952 30876 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31937 30876 603 41 0 31896 0
vsize: 127748
[startup+730.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 34398 0 0 0 72794 163 0 0 25 0 1 0 422268291 133103616 31430 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32496 31430 603 41 0 32455 0
vsize: 129984
[startup+740.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 34720 0 0 0 73793 164 0 0 25 0 1 0 422268291 134406144 31752 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32814 31752 603 41 0 32773 0
vsize: 131256
[startup+750.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 35127 0 0 0 74793 164 0 0 25 0 1 0 422268291 136089600 32159 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33225 32159 603 41 0 33184 0
vsize: 132900
[startup+760.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 35427 0 0 0 75792 165 0 0 25 0 1 0 422268291 137252864 32459 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33509 32459 603 41 0 33468 0
vsize: 134036
[startup+770.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 35885 0 0 0 76791 166 0 0 25 0 1 0 422268291 139194368 32917 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33983 32917 603 41 0 33942 0
vsize: 135932
[startup+780.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 36224 0 0 0 77790 167 0 0 25 0 1 0 422268291 140488704 33256 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34299 33256 603 41 0 34258 0
vsize: 137196
[startup+790.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 36650 0 0 0 78789 168 0 0 25 0 1 0 422268291 142290944 33682 4294967295 134512640 134672761 3221224560 3221223600 134614246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34739 33682 603 41 0 34698 0
vsize: 138956
[startup+800.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 37153 0 0 0 79789 169 0 0 25 0 1 0 422268291 144355328 34185 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35243 34185 603 41 0 35202 0
vsize: 140972
[startup+810.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 37513 0 0 0 80788 170 0 0 25 0 1 0 422268291 145793024 34545 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35594 34545 603 41 0 35553 0
vsize: 142376
[startup+820.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 37859 0 0 0 81787 171 0 0 25 0 1 0 422268291 147238912 34891 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35947 34891 603 41 0 35906 0
vsize: 143788
[startup+830.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 38096 0 0 0 82787 171 0 0 25 0 1 0 422268291 148168704 35128 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36174 35128 603 41 0 36133 0
vsize: 144696
[startup+840.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 38492 0 0 0 83786 172 0 0 25 0 1 0 422268291 149753856 35524 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36561 35524 603 41 0 36520 0
vsize: 146244
[startup+850 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 39133 0 0 0 84784 174 0 0 25 0 1 0 422268291 152477696 36165 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37226 36165 603 41 0 37185 0
vsize: 148904
[startup+860.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 39468 0 0 0 85784 175 0 0 25 0 1 0 422268291 153804800 36500 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37550 36500 603 41 0 37509 0
vsize: 150200
[startup+870.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 39814 0 0 0 86783 176 0 0 25 0 1 0 422268291 155246592 36846 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37902 36846 603 41 0 37861 0
vsize: 151608
[startup+880.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 40437 0 0 0 87782 177 0 0 25 0 1 0 422268291 157802496 37469 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38526 37469 603 41 0 38485 0
vsize: 154104
[startup+890.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 40830 0 0 0 88782 178 0 0 25 0 1 0 422268291 159375360 37862 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38910 37862 603 41 0 38869 0
vsize: 155640
[startup+900.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 41211 0 0 0 89781 179 0 0 25 0 1 0 422268291 160907264 38243 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39284 38243 603 41 0 39243 0
vsize: 157136
[startup+910.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 41874 0 0 0 90780 180 0 0 25 0 1 0 422268291 163659776 38906 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39956 38906 603 41 0 39915 0
vsize: 159824
[startup+920.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 42489 0 0 0 91778 182 0 0 25 0 1 0 422268291 166154240 39521 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40565 39521 603 41 0 40524 0
vsize: 162260
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 42924 0 0 0 92777 183 0 0 25 0 1 0 422268291 167903232 39956 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40992 39956 603 41 0 40951 0
vsize: 163968
[startup+940.002 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 43190 0 0 0 93777 184 0 0 25 0 1 0 422268291 168935424 40222 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41244 40222 603 41 0 41203 0
vsize: 164976
[startup+950.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 43586 0 0 0 94776 185 0 0 25 0 1 0 422268291 170651648 40618 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41663 40618 603 41 0 41622 0
vsize: 166652
[startup+960.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 43945 0 0 0 95775 186 0 0 25 0 1 0 422268291 172105728 40977 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42018 40977 603 41 0 41977 0
vsize: 168072
[startup+970.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 44222 0 0 0 96775 186 0 0 25 0 1 0 422268291 173260800 41254 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42300 41254 603 41 0 42259 0
vsize: 169200
[startup+980.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 44618 0 0 0 97774 187 0 0 25 0 1 0 422268291 174858240 41650 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42690 41650 603 41 0 42649 0
vsize: 170760
[startup+990.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 45241 0 0 0 98772 189 0 0 25 0 1 0 422268291 177336320 42273 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43295 42273 603 41 0 43254 0
vsize: 173180
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 45362 0 0 0 99772 189 0 0 25 0 1 0 422268291 177852416 42394 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43421 42394 603 41 0 43380 0
vsize: 173684
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 45740 0 0 0 100772 190 0 0 25 0 1 0 422268291 179437568 42772 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43808 42772 603 41 0 43767 0
vsize: 175232
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 46035 0 0 0 101771 191 0 0 25 0 1 0 422268291 180617216 43067 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44096 43067 603 41 0 44055 0
vsize: 176384
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 46573 0 0 0 102770 192 0 0 25 0 1 0 422268291 182800384 43605 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44629 43605 603 41 0 44588 0
vsize: 178516
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 46764 0 0 0 103769 193 0 0 25 0 1 0 422268291 183590912 43796 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44822 43796 603 41 0 44781 0
vsize: 179288
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 46997 0 0 0 104769 194 0 0 25 0 1 0 422268291 184500224 44029 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45044 44029 603 41 0 45003 0
vsize: 180176
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 47678 0 0 0 105768 195 0 0 25 0 1 0 422268291 187285504 44710 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45724 44710 603 41 0 45683 0
vsize: 182896
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 48172 0 0 0 106767 196 0 0 25 0 1 0 422268291 189362176 45204 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46231 45204 603 41 0 46190 0
vsize: 184924
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 48500 0 0 0 107767 197 0 0 25 0 1 0 422268291 190660608 45532 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46548 45532 603 41 0 46507 0
vsize: 186192
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 49176 0 0 0 108766 198 0 0 25 0 1 0 422268291 193404928 46208 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47218 46208 603 41 0 47177 0
vsize: 188872
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 49689 0 0 0 109765 199 0 0 25 0 1 0 422268291 195604480 46721 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47755 46721 603 41 0 47714 0
vsize: 191020
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 50014 0 0 0 110765 199 0 0 25 0 1 0 422268291 196857856 47046 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48061 47046 603 41 0 48020 0
vsize: 192244
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 50463 0 0 0 111764 200 0 0 25 0 1 0 422268291 198684672 47495 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48507 47495 603 41 0 48466 0
vsize: 194028
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 50708 0 0 0 112764 200 0 0 25 0 1 0 422268291 199737344 47740 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48764 47740 603 41 0 48723 0
vsize: 195056
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 51216 0 0 0 113763 202 0 0 25 0 1 0 422268291 201838592 48248 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49277 48248 603 41 0 49236 0
vsize: 197108
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 51598 0 0 0 114762 203 0 0 25 0 1 0 422268291 203407360 48630 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49660 48630 603 41 0 49619 0
vsize: 198640
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 51957 0 0 0 115762 203 0 0 25 0 1 0 422268291 204853248 48989 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50013 48989 603 41 0 49972 0
vsize: 200052
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 52213 0 0 0 116761 204 0 0 25 0 1 0 422268291 205860864 49245 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50259 49245 603 41 0 50218 0
vsize: 201036
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 52571 0 0 0 117761 205 0 0 25 0 1 0 422268291 207298560 49603 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50610 49603 603 41 0 50569 0
vsize: 202440
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 52752 0 0 0 118761 205 0 0 25 0 1 0 422268291 208023552 49784 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50787 49784 603 41 0 50746 0
vsize: 203148
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 52997 0 0 0 119760 205 0 0 25 0 1 0 422268291 209059840 50029 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51040 50029 603 41 0 50999 0
vsize: 204160
[startup+1210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27175
Raw data (stat): 27173 (minisat+) R 27172 22932 22931 0 -1 0 53193 0 0 0 120760 206 0 0 25 0 1 0 422268291 209846272 50225 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51232 50225 603 41 0 51191 0
vsize: 204928
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27175
Raw data (stat): 27173 (minisat+) Z 27172 22932 22931 0 -1 12 53194 0 0 0 120760 220 0 0 25 0 1 0 422268291 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.15
CPU time (s): 1209.81
CPU user time (s): 1207.61
CPU system time (s): 2.20267
CPU usage (%): 99.9718
Max. virtual memory (Kb): 204928
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####