PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        885628 kB
Buffers:         34444 kB
Cached:          78520 kB
SwapCached:       2636 kB
Active:          49744 kB
Inactive:        68704 kB
HighTotal:      131008 kB
HighFree:        48776 kB
LowTotal:       903652 kB
LowFree:        836852 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            25016 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:21:24 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 4093 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58579 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 |   58579   117158 |   17573       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   58579   117158 |   23431       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 2.72159 s)
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  104196   224283 |   31258       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/31196          
c   -- var.elim.:  2000/31196          
c   -- var.elim.:  3000/31196          
c   -- var.elim.:  4000/31196          
c   -- var.elim.:  5000/31196          
c   -- var.elim.:  6000/31196          
c   -- var.elim.:  7000/31196          
c   -- var.elim.:  8000/31196          
c   -- var.elim.:  9000/31196          
c   -- var.elim.:  10000/31196          
c   -- var.elim.:  11000/31196          
c   -- var.elim.:  12000/31196          
c   -- var.elim.:  13000/31196          
c   -- var.elim.:  14000/31196          
c   -- var.elim.:  15000/31196          
c   -- var.elim.:  16000/31196          
c   -- var.elim.:  17000/31196          
c   -- var.elim.:  18000/31196          
c   -- var.elim.:  19000/31196          
c   -- var.elim.:  20000/31196          
c   -- var.elim.:  21000/31196          
c   -- var.elim.:  22000/31196          
c   -- var.elim.:  23000/31196          
c   -- var.elim.:  24000/31196          
c   -- var.elim.:  25000/31196          
c   -- var.elim.:  26000/31196          
c   -- var.elim.:  27000/31196          
c   -- var.elim.:  28000/31196          
c   -- var.elim.:  29000/31196          
c   -- var.elim.:  30000/31196          
c   -- var.elim.:  31000/31196          
c   -- var.elim.:  31196/31196          
c   -- var.elim.:  1000/15828          
c   -- var.elim.:  2000/15828          
c   -- var.elim.:  3000/15828          
c   -- var.elim.:  4000/15828          
c   -- var.elim.:  5000/15828          
c   -- var.elim.:  6000/15828          
c   -- var.elim.:  7000/15828          
c   -- var.elim.:  8000/15828          
c   -- var.elim.:  9000/15828          
c   -- var.elim.:  10000/15828          
c   -- var.elim.:  11000/15828          
c   -- var.elim.:  12000/15828          
c   -- var.elim.:  13000/15828          
c   -- var.elim.:  14000/15828          
c   -- var.elim.:  15000/15828          
c   -- var.elim.:  15828/15828          
c   -- var.elim.:  1000/2517          
c   -- var.elim.:  2000/2517          
c   -- var.elim.:  2517/2517          
c   -- subsuming                       
c   -- var.elim.:  1000/6089          
c   -- var.elim.:  2000/6089          
c   -- var.elim.:  3000/6089          
c   -- var.elim.:  4000/6089          
c   -- var.elim.:  5000/6089          
c   -- var.elim.:  6000/6089          
c   -- var.elim.:  6089/6089          
c   -- var.elim.:  635/635          
c   -- subsuming                       
c   -- var.elim.:  469/469          
c |         0 |   71849   223850 |      --       0       --      -- |     --   | -32347/-432
c |         0 |   71849   223850 |   28739       0        0     nan |  0.000 % |
c |       100 |   71833   223713 |   31606      99    12373   125.0 | 53.330 % |
c |       250 |   71833   223713 |   34767     249    49856   200.2 | 53.330 % |
c |       475 |   71833   223713 |   38243     474    85353   180.1 | 53.330 % |
c |       812 |   71833   223713 |   42068     811   166492   205.3 | 53.330 % |
c |      1318 |   71833   223713 |   46275    1317   276274   209.8 | 53.330 % |
c |      2077 |   71813   223517 |   50888    2074   436419   210.4 | 53.393 % |
c |      3217 |   71813   223517 |   55977    3214   656767   204.3 | 53.393 % |
c |      4926 |   71733   222768 |   61506    4918  1007937   204.9 | 53.647 % |
c |      7488 |   71696   222350 |   67622    7470  1594650   213.5 | 53.761 % |
c |     11333 |   71451   220083 |   74130   11297  2644787   234.1 | 54.484 % |
c ==============================================================================
c (current CPU-time: 115.467 s)
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14395 |   78571   237655 |   23571   14326  3580622   249.9 | 54.484 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14064          
c   -- var.elim.:  2000/14064          
c   -- var.elim.:  3000/14064          
c   -- var.elim.:  4000/14064          
c   -- var.elim.:  5000/14064          
c   -- var.elim.:  6000/14064          
c   -- var.elim.:  7000/14064          
c   -- var.elim.:  8000/14064          
c   -- var.elim.:  9000/14064          
c   -- var.elim.:  10000/14064          
c   -- var.elim.:  11000/14064          
c   -- var.elim.:  12000/14064          
c   -- var.elim.:  13000/14064          
c   -- var.elim.:  14000/14064          
c   -- var.elim.:  14064/14064          
c   -- var.elim.:  1000/5445          
c   -- var.elim.:  2000/5445          
c   -- var.elim.:  3000/5445          
c   -- var.elim.:  4000/5445          
c   -- var.elim.:  5000/5445          
c   -- var.elim.:  5445/5445          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/4419          
c   -- var.elim.:  2000/4419          
c   -- var.elim.:  3000/4419          
c   -- var.elim.:  4000/4419          
c   -- var.elim.:  4419/4419          
c   -- var.elim.:  809/809          
c |     14395 |   71282   224832 |      --   14326       --      -- |     --   | -7272/-11411
c |     14395 |   71282   224832 |   28512   13137  2480887   188.8 | 54.484 % |
c |     14496 |   71282   224832 |   31364   13238  2502304   189.0 | 63.169 % |
c |     14649 |   71282   224832 |   34500   13391  2535641   189.4 | 63.169 % |
c |     14874 |   71282   224832 |   37950   13616  2590531   190.3 | 63.169 % |
c |     15211 |   71282   224832 |   41745   13953  2652257   190.1 | 63.169 % |
c |     15718 |   71282   224832 |   45920   14460  2809058   194.3 | 63.169 % |
c |     16477 |   71244   224422 |   50485   15214  3005736   197.6 | 63.268 % |
c |     17616 |   71196   223917 |   55496   16345  3335229   204.1 | 63.393 % |
c |     19324 |   71166   223672 |   61020   18045  3795988   210.4 | 63.471 % |
c |     21887 |   71064   222716 |   67026   20591  4470284   217.1 | 63.736 % |
c |     25731 |   70992   222044 |   73653   24415  5672693   232.3 | 63.923 % |
c |     31497 |   70850   220688 |   80857   30166  7435030   246.5 | 64.287 % |
c |     40146 |   70794   220188 |   88872   38798 10402537   268.1 | 64.433 % |
c |     53122 |   70306   215551 |   97086   51661 14798774   286.5 | 65.701 % |
c |     72583 |   69832   211297 |  106074   70982 22057614   310.7 | 66.923 % |
c ==============================================================================
c (current CPU-time: 505.53 s)
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     80368 |   71919   214762 |   21575   78649 24836921   315.8 | 66.923 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7729          
c   -- var.elim.:  2000/7729          
c   -- var.elim.:  3000/7729          
c   -- var.elim.:  4000/7729          
c   -- var.elim.:  5000/7729          
c   -- var.elim.:  6000/7729          
c   -- var.elim.:  7000/7729          
c   -- var.elim.:  7729/7729          
c   -- var.elim.:  1000/1640          
c   -- var.elim.:  1640/1640          
c   -- var.elim.:  443/443          
c |     80368 |   69538   211044 |      --   78649       --      -- |     --   | -2381/-3717
c |     80368 |   69538   211044 |   27815   78649 24836921   315.8 | 66.923 % |
c |     80468 |   69538   211044 |   30596   23678  4800077   202.7 | 68.175 % |
c |     80618 |   69538   211044 |   33656   23828  4838279   203.1 | 68.175 % |
c |     80843 |   69485   210582 |   36993   24050  4901911   203.8 | 68.309 % |
c |     81180 |   69455   210306 |   40675   24386  4974797   204.0 | 68.380 % |
c |     81686 |   69455   210306 |   44743   24892  5140350   206.5 | 68.380 % |
c |     82445 |   69455   210306 |   49217   25651  5325692   207.6 | 68.380 % |
c |     83584 |   69425   210046 |   54115   26783  5657748   211.2 | 68.457 % |
c |     85292 |   69327   209171 |   59443   28484  6257062   219.7 | 68.699 % |
c |     87855 |   69291   208872 |   65353   31041  7111497   229.1 | 68.791 % |
c |     91700 |   69145   207540 |   71737   34862  8445718   242.3 | 69.155 % |
c |     97467 |   68995   206152 |   78740   40607 10484194   258.2 | 69.535 % |
c |    106118 |   68704   203617 |   86249   49209 13537837   275.1 | 70.258 % |
c |    119092 |   68499   200873 |   94590   62151 18418592   296.4 | 70.756 % |
c |    138556 |   67920   195667 |  103170   81442 25402653   311.9 | 72.187 % |
c |    167748 |   67362   190981 |  112555  110504 36679014   331.9 | 73.567 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 C925 -C924 -C923 C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 C738 -C737 -C736 -C735 -C734 C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 C694 C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -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 -C466 C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 C382 -C381 -C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239#### 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.95 0.97 0.91 2/54 32366
Raw data (stat): 32366 (runsolver) R 32365 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480469036 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 6509 0 0 0 971 27 0 0 25 0 1 0 480469036 26873856 6097 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6561 6097 603 41 0 6520 0
vsize: 26244
[startup+20.0018 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 6521 0 0 0 1971 28 0 0 25 0 1 0 480469036 27058176 6109 4294967295 134512640 134672761 3221224560 3221223056 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6606 6109 603 41 0 6565 0
vsize: 26424
[startup+30.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 6527 0 0 0 2971 28 0 0 25 0 1 0 480469036 27058176 6115 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6606 6115 603 41 0 6565 0
vsize: 26424
[startup+40.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 6539 0 0 0 3970 28 0 0 25 0 1 0 480469036 27058176 6127 4294967295 134512640 134672761 3221224560 3221223056 134644266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6606 6127 603 41 0 6565 0
vsize: 26424
[startup+50.0037 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 6558 0 0 0 4970 29 0 0 25 0 1 0 480469036 27058176 6146 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6606 6146 603 41 0 6565 0
vsize: 26424
[startup+60.0033 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 6564 0 0 0 5970 29 0 0 25 0 1 0 480469036 27058176 6152 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6606 6152 603 41 0 6565 0
vsize: 26424
[startup+70.0047 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 6768 0 0 0 6969 29 0 0 25 0 1 0 480469036 28008448 6356 4294967295 134512640 134672761 3221224560 3221223120 134607795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6838 6356 603 41 0 6797 0
vsize: 27352
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 6768 0 0 0 7968 30 0 0 25 0 1 0 480469036 27058176 6152 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6606 6152 603 41 0 6565 0
vsize: 26424
[startup+90.0053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 7555 0 0 0 8967 31 0 0 25 0 1 0 480469036 29523968 6735 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7208 6735 603 41 0 7167 0
vsize: 28832
[startup+100.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 8648 0 0 0 9964 34 0 0 25 0 1 0 480469036 33947648 7828 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8288 7828 603 41 0 8247 0
vsize: 33152
[startup+110.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 9655 0 0 0 10961 37 0 0 25 0 1 0 480469036 38178816 8835 4294967295 134512640 134672761 3221224560 3221223408 134605846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8835 603 41 0 9280 0
vsize: 37284
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 11838 0 0 0 11940 58 0 0 25 0 1 0 480469036 44990464 10027 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10027 603 41 0 10943 0
vsize: 43936
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 11838 0 0 0 12931 68 0 0 25 0 1 0 480469036 44990464 10027 4294967295 134512640 134672761 3221224560 3221222976 134631392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10984 10027 603 41 0 10943 0
vsize: 43936
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 12042 0 0 0 13930 68 0 0 25 0 1 0 480469036 44990464 10027 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10984 10027 603 41 0 10943 0
vsize: 43936
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 12043 0 0 0 14930 68 0 0 25 0 1 0 480469036 44990464 10028 4294967295 134512640 134672761 3221224560 3221223472 134644266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10984 10028 603 41 0 10943 0
vsize: 43936
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 12410 0 0 0 15929 69 0 0 25 0 1 0 480469036 46538752 10395 4294967295 134512640 134672761 3221224560 3221223696 134614560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11362 10395 603 41 0 11321 0
vsize: 45448
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 13364 0 0 0 16927 72 0 0 25 0 1 0 480469036 50434048 11349 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12313 11349 603 41 0 12272 0
vsize: 49252
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 14259 0 0 0 17925 74 0 0 25 0 1 0 480469036 54161408 12244 4294967295 134512640 134672761 3221224560 3221223600 134613768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13223 12244 603 41 0 13182 0
vsize: 52892
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 14938 0 0 0 18924 76 0 0 25 0 1 0 480469036 56897536 12923 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13891 12923 603 41 0 13850 0
vsize: 55564
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 15904 0 0 0 19921 78 0 0 25 0 1 0 480469036 60805120 13889 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14845 13889 603 41 0 14804 0
vsize: 59380
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 16830 0 0 0 20919 81 0 0 25 0 1 0 480469036 64851968 14815 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15833 14815 603 41 0 15792 0
vsize: 63332
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 17714 0 0 0 21917 83 0 0 25 0 1 0 480469036 68448256 15699 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16711 15699 603 41 0 16670 0
vsize: 66844
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 18529 0 0 0 22915 85 0 0 25 0 1 0 480469036 71712768 16514 4294967295 134512640 134672761 3221224560 3221223600 134612791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17508 16514 603 41 0 17467 0
vsize: 70032
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 19233 0 0 0 23914 86 0 0 25 0 1 0 480469036 74539008 17218 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18198 17218 603 41 0 18157 0
vsize: 72792
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32366
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 19892 0 0 0 24913 88 0 0 25 0 1 0 480469036 77246464 17877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18859 17877 603 41 0 18818 0
vsize: 75436
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 20478 0 0 0 25911 89 0 0 25 0 1 0 480469036 79675392 18463 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19452 18463 603 41 0 19411 0
vsize: 77808
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 21023 0 0 0 26911 89 0 0 25 0 1 0 480469036 81870848 19008 4294967295 134512640 134672761 3221224560 3221223724 134564508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19988 19008 603 41 0 19947 0
vsize: 79952
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 21727 0 0 0 27909 91 0 0 25 0 1 0 480469036 84840448 19712 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19712 603 41 0 20672 0
vsize: 82852
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 22413 0 0 0 28907 94 0 0 25 0 1 0 480469036 87592960 20398 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21385 20398 603 41 0 21344 0
vsize: 85540
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 23008 0 0 0 29907 95 0 0 25 0 1 0 480469036 89968640 20993 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21965 20993 603 41 0 21924 0
vsize: 87860
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 23707 0 0 0 30905 96 0 0 25 0 1 0 480469036 92930048 21692 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22688 21692 603 41 0 22647 0
vsize: 90752
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 24388 0 0 0 31904 97 0 0 25 0 1 0 480469036 95637504 22373 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23349 22373 603 41 0 23308 0
vsize: 93396
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 25025 0 0 0 32903 99 0 0 25 0 1 0 480469036 98254848 23010 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23988 23010 603 41 0 23947 0
vsize: 95952
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 25554 0 0 0 33901 101 0 0 25 0 1 0 480469036 100462592 23539 4294967295 134512640 134672761 3221224560 3221223744 134615985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24527 23539 603 41 0 24486 0
vsize: 98108
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 26201 0 0 0 34899 102 0 0 25 0 1 0 480469036 103120896 24186 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25176 24186 603 41 0 25135 0
vsize: 100704
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 26835 0 0 0 35897 105 0 0 25 0 1 0 480469036 105668608 24820 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25798 24820 603 41 0 25757 0
vsize: 103192
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 27330 0 0 0 36896 106 0 0 25 0 1 0 480469036 107626496 25315 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26276 25315 603 41 0 26235 0
vsize: 105104
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 27654 0 0 0 37896 107 0 0 25 0 1 0 480469036 108941312 25639 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26597 25639 603 41 0 26556 0
vsize: 106388
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 28333 0 0 0 38894 108 0 0 25 0 1 0 480469036 111828992 26318 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27302 26318 603 41 0 27261 0
vsize: 109208
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 28703 0 0 0 39893 110 0 0 25 0 1 0 480469036 113594368 26688 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27733 26688 603 41 0 27692 0
vsize: 110932
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 29470 0 0 0 40891 112 0 0 25 0 1 0 480469036 116727808 27455 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28498 27455 603 41 0 28457 0
vsize: 113992
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 29971 0 0 0 41890 113 0 0 25 0 1 0 480469036 118697984 27956 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28979 27956 603 41 0 28938 0
vsize: 115916
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 30618 0 0 0 42889 115 0 0 25 0 1 0 480469036 121405440 28603 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29640 28603 603 41 0 29599 0
vsize: 118560
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 30896 0 0 0 43888 115 0 0 25 0 1 0 480469036 122449920 28881 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29895 28881 603 41 0 29854 0
vsize: 119580
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 31339 0 0 0 44888 116 0 0 25 0 1 0 480469036 124358656 29324 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30361 29324 603 41 0 30320 0
vsize: 121444
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 31976 0 0 0 45887 117 0 0 25 0 1 0 480469036 126967808 29961 4294967295 134512640 134672761 3221224560 3221223704 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30998 29961 603 41 0 30957 0
vsize: 123992
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 32288 0 0 0 46885 119 0 0 25 0 1 0 480469036 128155648 30273 4294967295 134512640 134672761 3221224560 3221223704 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31288 30273 603 41 0 31247 0
vsize: 125152
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 32776 0 0 0 47884 120 0 0 25 0 1 0 480469036 130138112 30761 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31772 30761 603 41 0 31731 0
vsize: 127088
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 33183 0 0 0 48883 121 0 0 25 0 1 0 480469036 131850240 31168 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32190 31168 603 41 0 32149 0
vsize: 128760
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 33549 0 0 0 49883 122 0 0 25 0 1 0 480469036 133402624 31534 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32569 31534 603 41 0 32528 0
vsize: 130276
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35555 0 0 0 50874 132 0 0 25 0 1 0 480469036 136241152 32102 4294967295 134512640 134672761 3221224560 3221223104 134621202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33262 32102 603 41 0 33221 0
vsize: 133048
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35698 0 0 0 51868 137 0 0 25 0 1 0 480469036 134852608 31955 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31955 603 41 0 32882 0
vsize: 131692
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35698 0 0 0 52868 137 0 0 25 0 1 0 480469036 134852608 31955 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31955 603 41 0 32882 0
vsize: 131692
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 53869 137 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 54869 137 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 55869 137 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 56869 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 57869 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 58869 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 59869 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 60870 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 61870 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 62870 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 63870 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223728 134564729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 64870 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 65870 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 66870 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 67871 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223760 134610630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 68871 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223812 134617908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 69871 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 70871 138 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 71871 139 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 72871 139 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223600 134614207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35699 0 0 0 73871 139 0 0 25 0 1 0 480469036 134852608 31956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31956 603 41 0 32882 0
vsize: 131692
[startup+750.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 74872 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 75872 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 76872 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 77872 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+790.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 78872 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 79872 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+810.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 80872 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223336 1075352052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 81873 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 82873 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35700 0 0 0 83873 139 0 0 25 0 1 0 480469036 134852608 31957 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31957 603 41 0 32882 0
vsize: 131692
[startup+850.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35701 0 0 0 84873 139 0 0 25 0 1 0 480469036 134852608 31958 4294967295 134512640 134672761 3221224560 3221223432 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32923 31958 603 41 0 32882 0
vsize: 131692
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 35921 0 0 0 85872 140 0 0 25 0 1 0 480469036 135782400 32178 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33150 32178 603 41 0 33109 0
vsize: 132600
[startup+870.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 36441 0 0 0 86871 142 0 0 25 0 1 0 480469036 137990144 32698 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33689 32698 603 41 0 33648 0
vsize: 134756
[startup+880.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 36786 0 0 0 87870 142 0 0 25 0 1 0 480469036 139300864 33043 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34009 33043 603 41 0 33968 0
vsize: 136036
[startup+890.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 37282 0 0 0 88868 144 0 0 25 0 1 0 480469036 141385728 33539 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34518 33539 603 41 0 34477 0
vsize: 138072
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 37930 0 0 0 89867 146 0 0 25 0 1 0 480469036 143986688 34187 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35153 34187 603 41 0 35112 0
vsize: 140612
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 38550 0 0 0 90865 148 0 0 25 0 1 0 480469036 146567168 34807 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35783 34807 603 41 0 35742 0
vsize: 143132
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 38914 0 0 0 91865 149 0 0 25 0 1 0 480469036 148119552 35171 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36162 35171 603 41 0 36121 0
vsize: 144648
[startup+930.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 39247 0 0 0 92864 150 0 0 25 0 1 0 480469036 149417984 35504 4294967295 134512640 134672761 3221224560 3221223704 134616108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36479 35504 603 41 0 36438 0
vsize: 145916
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 39665 0 0 0 93863 151 0 0 25 0 1 0 480469036 151101440 35922 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36890 35922 603 41 0 36849 0
vsize: 147560
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 39971 0 0 0 94862 152 0 0 25 0 1 0 480469036 152420352 36228 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37212 36228 603 41 0 37171 0
vsize: 148848
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 40282 0 0 0 95862 153 0 0 25 0 1 0 480469036 153718784 36539 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37529 36539 603 41 0 37488 0
vsize: 150116
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 40986 0 0 0 96860 154 0 0 25 0 1 0 480469036 156561408 37243 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38223 37243 603 41 0 38182 0
vsize: 152892
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 41417 0 0 0 97859 155 0 0 25 0 1 0 480469036 158363648 37674 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38663 37674 603 41 0 38622 0
vsize: 154652
[startup+990.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 41782 0 0 0 98858 156 0 0 25 0 1 0 480469036 159809536 38039 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39016 38039 603 41 0 38975 0
vsize: 156064
[startup+1000.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 42060 0 0 0 99858 157 0 0 25 0 1 0 480469036 160980992 38317 4294967295 134512640 134672761 3221224560 3221223704 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39302 38317 603 41 0 39261 0
vsize: 157208
[startup+1010.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 42567 0 0 0 100856 158 0 0 25 0 1 0 480469036 163078144 38824 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39814 38824 603 41 0 39773 0
vsize: 159256
[startup+1020.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 43034 0 0 0 101855 160 0 0 25 0 1 0 480469036 164904960 39291 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40260 39291 603 41 0 40219 0
vsize: 161040
[startup+1030.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 43516 0 0 0 102854 161 0 0 25 0 1 0 480469036 166871040 39773 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40740 39773 603 41 0 40699 0
vsize: 162960
[startup+1040.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 44040 0 0 0 103853 162 0 0 25 0 1 0 480469036 169078784 40297 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41279 40297 603 41 0 41238 0
vsize: 165116
[startup+1050.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 44598 0 0 0 104852 163 0 0 25 0 1 0 480469036 171311104 40855 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41824 40855 603 41 0 41783 0
vsize: 167296
[startup+1060.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 45218 0 0 0 105851 165 0 0 25 0 1 0 480469036 173916160 41475 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42460 41475 603 41 0 42419 0
vsize: 169840
[startup+1070.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 45647 0 0 0 106849 167 0 0 25 0 1 0 480469036 175603712 41904 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42872 41904 603 41 0 42831 0
vsize: 171488
[startup+1080.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 46086 0 0 0 107848 168 0 0 25 0 1 0 480469036 177463296 42343 4294967295 134512640 134672761 3221224560 3221223704 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43326 42343 603 41 0 43285 0
vsize: 173304
[startup+1090.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 46405 0 0 0 108847 169 0 0 25 0 1 0 480469036 178753536 42662 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43641 42662 603 41 0 43600 0
vsize: 174564
[startup+1100.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 46958 0 0 0 109846 170 0 0 25 0 1 0 480469036 180965376 43215 4294967295 134512640 134672761 3221224560 3221223704 134616284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44181 43215 603 41 0 44140 0
vsize: 176724
[startup+1110.03 s]
Raw data (loadavg): 1.16 1.02 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 47324 0 0 0 110845 171 0 0 25 0 1 0 480469036 182521856 43581 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44561 43581 603 41 0 44520 0
vsize: 178244
[startup+1120.03 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 47954 0 0 0 111844 172 0 0 25 0 1 0 480469036 185090048 44211 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45188 44211 603 41 0 45147 0
vsize: 180752
[startup+1130.03 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 48226 0 0 0 112844 173 0 0 25 0 1 0 480469036 186155008 44483 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45448 44483 603 41 0 45407 0
vsize: 181792
[startup+1140.03 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 48738 0 0 0 113843 174 0 0 25 0 1 0 480469036 188252160 44995 4294967295 134512640 134672761 3221224560 3221223704 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45960 44995 603 41 0 45919 0
vsize: 183840
[startup+1150.03 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 49064 0 0 0 114843 175 0 0 25 0 1 0 480469036 189571072 45321 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46282 45321 603 41 0 46241 0
vsize: 185128
[startup+1160.03 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 49314 0 0 0 115842 175 0 0 25 0 1 0 480469036 190623744 45571 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46539 45571 603 41 0 46498 0
vsize: 186156
[startup+1170.03 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 49676 0 0 0 116842 176 0 0 25 0 1 0 480469036 192077824 45933 4294967295 134512640 134672761 3221224560 3221223728 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46894 45933 603 41 0 46853 0
vsize: 187576
[startup+1180.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 50080 0 0 0 117841 177 0 0 25 0 1 0 480469036 193740800 46337 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47300 46337 603 41 0 47259 0
vsize: 189200
[startup+1190.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 50405 0 0 0 118840 178 0 0 25 0 1 0 480469036 195051520 46662 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47620 46662 603 41 0 47579 0
vsize: 190480
[startup+1200.03 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 32368
Raw data (stat): 32366 (minisat+) R 32365 27565 27564 0 -1 0 51156 0 0 0 119839 179 0 0 25 0 1 0 480469036 198152192 47413 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48377 47413 603 41 0 48336 0
vsize: 193508
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.03 1.01 0.93 1/54 32368
Raw data (stat): 32366 (minisat+) Z 32365 27565 27564 0 -1 12 51157 0 0 0 119839 190 0 0 25 0 1 0 480469036 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.14
CPU time (s): 1200.3
CPU user time (s): 1198.4
CPU system time (s): 1.90371
CPU usage (%): 100.013
Max. virtual memory (Kb): 193508
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####