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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        833076 kB
Buffers:         34716 kB
Cached:         123976 kB
SwapCached:       3828 kB
Active:          53548 kB
Inactive:       111840 kB
HighTotal:      131008 kB
HighFree:         4732 kB
LowTotal:       903652 kB
LowFree:        828344 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30592 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:27:36 (client local time) WITH STATUS 10 IN 1209.56 SECONDS
stats: 4103 7 1209.56 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94226 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 |   94226   188452 |   28267       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   94226   188452 |   37690       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 5.37918 s)
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70300     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  169278   364519 |   50783       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/51085          
c   -- var.elim.:  2000/51085          
c   -- var.elim.:  3000/51085          
c   -- var.elim.:  4000/51085          
c   -- var.elim.:  5000/51085          
c   -- var.elim.:  6000/51085          
c   -- var.elim.:  7000/51085          
c   -- var.elim.:  8000/51085          
c   -- var.elim.:  9000/51085          
c   -- var.elim.:  10000/51085          
c   -- var.elim.:  11000/51085          
c   -- var.elim.:  12000/51085          
c   -- var.elim.:  13000/51085          
c   -- var.elim.:  14000/51085          
c   -- var.elim.:  15000/51085          
c   -- var.elim.:  16000/51085          
c   -- var.elim.:  17000/51085          
c   -- var.elim.:  18000/51085          
c   -- var.elim.:  19000/51085          
c   -- var.elim.:  20000/51085          
c   -- var.elim.:  21000/51085          
c   -- var.elim.:  22000/51085          
c   -- var.elim.:  23000/51085          
c   -- var.elim.:  24000/51085          
c   -- var.elim.:  25000/51085          
c   -- var.elim.:  26000/51085          
c   -- var.elim.:  27000/51085          
c   -- var.elim.:  28000/51085          
c   -- var.elim.:  29000/51085          
c   -- var.elim.:  30000/51085          
c   -- var.elim.:  31000/51085          
c   -- var.elim.:  32000/51085          
c   -- var.elim.:  33000/51085          
c   -- var.elim.:  34000/51085          
c   -- var.elim.:  35000/51085          
c   -- var.elim.:  36000/51085          
c   -- var.elim.:  37000/51085          
c   -- var.elim.:  38000/51085          
c   -- var.elim.:  39000/51085          
c   -- var.elim.:  40000/51085          
c   -- var.elim.:  41000/51085          
c   -- var.elim.:  42000/51085          
c   -- var.elim.:  43000/51085          
c   -- var.elim.:  44000/51085          
c   -- var.elim.:  45000/51085          
c   -- var.elim.:  46000/51085          
c   -- var.elim.:  47000/51085          
c   -- var.elim.:  48000/51085          
c   -- var.elim.:  49000/51085          
c   -- var.elim.:  50000/51085          
c   -- var.elim.:  51000/51085          
c   -- var.elim.:  51085/51085          
c   -- var.elim.:  1000/25894          
c   -- var.elim.:  2000/25894          
c   -- var.elim.:  3000/25894          
c   -- var.elim.:  4000/25894          
c   -- var.elim.:  5000/25894          
c   -- var.elim.:  6000/25894          
c   -- var.elim.:  7000/25894          
c   -- var.elim.:  8000/25894          
c   -- var.elim.:  9000/25894          
c   -- var.elim.:  10000/25894          
c   -- var.elim.:  11000/25894          
c   -- var.elim.:  12000/25894          
c   -- var.elim.:  13000/25894          
c   -- var.elim.:  14000/25894          
c   -- var.elim.:  15000/25894          
c   -- var.elim.:  16000/25894          
c   -- var.elim.:  17000/25894          
c   -- var.elim.:  18000/25894          
c   -- var.elim.:  19000/25894          
c   -- var.elim.:  20000/25894          
c   -- var.elim.:  21000/25894          
c   -- var.elim.:  22000/25894          
c   -- var.elim.:  23000/25894          
c   -- var.elim.:  24000/25894          
c   -- var.elim.:  25000/25894          
c   -- var.elim.:  25894/25894          
c   -- var.elim.:  277/277          
c   -- var.elim.:  133/133          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  1000/9578          
c   -- var.elim.:  2000/9578          
c   -- var.elim.:  3000/9578          
c   -- var.elim.:  4000/9578          
c   -- var.elim.:  5000/9578          
c   -- var.elim.:  6000/9578          
c   -- var.elim.:  7000/9578          
c   -- var.elim.:  8000/9578          
c   -- var.elim.:  9000/9578          
c   -- var.elim.:  9578/9578          
c   -- var.elim.:  745/745          
c |         0 |  114589   370198 |      --       0       --      -- |     --   | -54683/5697
c |         0 |  114589   370198 |   45835       0        0     nan |  0.000 % |
c |       100 |  114575   370047 |   50413      98     4018    41.0 | 56.468 % |
c |       250 |  114575   370047 |   55454     248    20397    82.2 | 56.468 % |
c |       476 |  114575   370047 |   60999     474    78219   165.0 | 56.468 % |
c |       814 |  114559   369854 |   67090     809   143400   177.3 | 56.499 % |
c |      1320 |  114559   369854 |   73799    1315   236848   180.1 | 56.499 % |
c |      2079 |  114559   369854 |   81179    2074   396947   191.4 | 56.499 % |
c |      3218 |  114559   369854 |   89297    3213   713651   222.1 | 56.499 % |
c |      4927 |  114477   369000 |   98156    4911  1134462   231.0 | 56.658 % |
c ==============================================================================
c (current CPU-time: 297.502 s)
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7280 |  126114   399362 |   37834    7229  1671507   231.2 | 56.658 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22123          
c   -- var.elim.:  2000/22123          
c   -- var.elim.:  3000/22123          
c   -- var.elim.:  4000/22123          
c   -- var.elim.:  5000/22123          
c   -- var.elim.:  6000/22123          
c   -- var.elim.:  7000/22123          
c   -- var.elim.:  8000/22123          
c   -- var.elim.:  9000/22123          
c   -- var.elim.:  10000/22123          
c   -- var.elim.:  11000/22123          
c   -- var.elim.:  12000/22123          
c   -- var.elim.:  13000/22123          
c   -- var.elim.:  14000/22123          
c   -- var.elim.:  15000/22123          
c   -- var.elim.:  16000/22123          
c   -- var.elim.:  17000/22123          
c   -- var.elim.:  18000/22123          
c   -- var.elim.:  19000/22123          
c   -- var.elim.:  20000/22123          
c   -- var.elim.:  21000/22123          
c   -- var.elim.:  22000/22123          
c   -- var.elim.:  22123/22123          
c   -- var.elim.:  1000/8650          
c   -- var.elim.:  2000/8650          
c   -- var.elim.:  3000/8650          
c   -- var.elim.:  4000/8650          
c   -- var.elim.:  5000/8650          
c   -- var.elim.:  6000/8650          
c   -- var.elim.:  7000/8650          
c   -- var.elim.:  8000/8650          
c   -- var.elim.:  8650/8650          
c   -- var.elim.:  42/42          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/7159          
c   -- var.elim.:  2000/7159          
c   -- var.elim.:  3000/7159          
c   -- var.elim.:  4000/7159          
c   -- var.elim.:  5000/7159          
c   -- var.elim.:  6000/7159          
c   -- var.elim.:  7000/7159          
c   -- var.elim.:  7159/7159          
c   -- var.elim.:  134/134          
c |      7280 |  114428   378257 |      --    7229       --      -- |     --   | -11660/-18900
c |      7280 |  114428   378257 |   45771    7073  1492992   211.1 | 56.658 % |
c |      7380 |  114428   378257 |   50348    7173  1509603   210.5 | 64.783 % |
c |      7530 |  114428   378257 |   55383    7323  1548661   211.5 | 64.783 % |
c |      7755 |  114428   378257 |   60921    7548  1612784   213.7 | 64.783 % |
c |      8092 |  114410   378044 |   67003    7882  1678284   212.9 | 64.812 % |
c |      8598 |  114278   376756 |   73618    8375  1773807   211.8 | 65.021 % |
c |      9359 |  114252   376493 |   80961    9135  1941250   212.5 | 65.062 % |
c |     10498 |  114226   376239 |   89037   10262  2152612   209.8 | 65.103 % |
c |     12206 |  114114   375195 |   97845   11951  2504532   209.6 | 65.280 % |
c |     14768 |  113888   373117 |  107416   14471  3165085   218.7 | 65.637 % |
c |     18612 |  113544   369899 |  117801   18241  4114180   225.5 | 66.181 % |
c |     24378 |  112914   363956 |  128862   23904  5739229   240.1 | 67.177 % |
c |     33027 |  111994   355077 |  140594   32361  8289623   256.2 | 68.606 % |
c ==============================================================================
c (current CPU-time: 510.482 s)
c ==============================================================================
c [1mFound solution: -42[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 |     34330 |  114479   360474 |   34343   33649  8693320   258.4 | 68.606 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11124          
c   -- var.elim.:  2000/11124          
c   -- var.elim.:  3000/11124          
c   -- var.elim.:  4000/11124          
c   -- var.elim.:  5000/11124          
c   -- var.elim.:  6000/11124          
c   -- var.elim.:  7000/11124          
c   -- var.elim.:  8000/11124          
c   -- var.elim.:  9000/11124          
c   -- var.elim.:  10000/11124          
c   -- var.elim.:  11000/11124          
c   -- var.elim.:  11124/11124          
c   -- var.elim.:  1000/1938          
c   -- var.elim.:  1938/1938          
c |     34330 |  111833   353444 |      --   33649       --      -- |     --   | -2633/-5138
c |     34330 |  111833   353444 |   44733   33649  8693320   258.4 | 68.606 % |
c |     34430 |  111833   353444 |   49206   33749  8721949   258.4 | 69.225 % |
c |     34580 |  111777   352851 |   54100   33410  8163307   244.3 | 69.306 % |
c |     34805 |  111775   352829 |   59509   33634  8215731   244.3 | 69.309 % |
c |     35142 |  111775   352829 |   65459   33971  8323629   245.0 | 69.309 % |
c |     35648 |  111775   352829 |   72005   34477  8487928   246.2 | 69.309 % |
c |     36408 |  111689   352029 |   79145   35217  8721258   247.6 | 69.437 % |
c |     37547 |  111629   351382 |   87013   36327  9062158   249.5 | 69.528 % |
c |     39255 |  111388   349065 |   95508   38011  9552827   251.3 | 69.891 % |
c |     41818 |  111247   347685 |  104925   40485 10407334   257.1 | 70.101 % |
c |     45662 |  111247   347685 |  115418   44329 11667536   263.2 | 70.101 % |
c |     51428 |  110743   342531 |  126385   49951 13587630   272.0 | 70.871 % |
c |     60077 |  110117   336304 |  138237   58399 16540215   283.2 | 71.828 % |
c |     73051 |  109181   327389 |  150768   71082 20977702   295.1 | 73.265 % |
c |     92513 |  108482   320685 |  164784   90236 28670043   317.7 | 74.335 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 C821 -C820 -C819 -C818 -C817 -C816 -C815 C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 C724 -C723 -C722 -C721 -C720 -C719 -C718 C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 2138
Raw data (stat): 2138 (runsolver) R 2137 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480502418 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10082 0 0 0 960 39 0 0 25 0 1 0 480502418 43790336 9491 4294967295 134512640 134672761 3221224560 3221222736 134621548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10691 9491 603 41 0 10650 0
vsize: 42764
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10458 0 0 0 1957 42 0 0 25 0 1 0 480502418 45330432 9867 4294967295 134512640 134672761 3221224560 3221222816 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11067 9867 603 41 0 11026 0
vsize: 44268
[startup+30.0006 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10464 0 0 0 2957 42 0 0 25 0 1 0 480502418 45330432 9873 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11067 9873 603 41 0 11026 0
vsize: 44268
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10465 0 0 0 3957 42 0 0 25 0 1 0 480502418 45330432 9874 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11067 9874 603 41 0 11026 0
vsize: 44268
[startup+50.001 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10466 0 0 0 4957 42 0 0 25 0 1 0 480502418 45330432 9875 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11067 9875 603 41 0 11026 0
vsize: 44268
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10467 0 0 0 5958 42 0 0 25 0 1 0 480502418 45330432 9876 4294967295 134512640 134672761 3221224560 3221223152 134607995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11067 9876 603 41 0 11026 0
vsize: 44268
[startup+70.0019 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10468 0 0 0 6958 42 0 0 25 0 1 0 480502418 45330432 9877 4294967295 134512640 134672761 3221224560 3221223088 134606396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11067 9877 603 41 0 11026 0
vsize: 44268
[startup+80.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10468 0 0 0 7958 42 0 0 25 0 1 0 480502418 45330432 9877 4294967295 134512640 134672761 3221224560 3221223056 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11067 9877 603 41 0 11026 0
vsize: 44268
[startup+90.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10501 0 0 0 8958 42 0 0 25 0 1 0 480502418 45592576 9910 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 9910 603 41 0 11090 0
vsize: 44524
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10503 0 0 0 9958 42 0 0 25 0 1 0 480502418 45592576 9912 4294967295 134512640 134672761 3221224560 3221222992 134604055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 9912 603 41 0 11090 0
vsize: 44524
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10504 0 0 0 10959 42 0 0 25 0 1 0 480502418 45592576 9913 4294967295 134512640 134672761 3221224560 3221223088 134607032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 9913 603 41 0 11090 0
vsize: 44524
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10505 0 0 0 11959 42 0 0 25 0 1 0 480502418 45592576 9914 4294967295 134512640 134672761 3221224560 3221223056 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 9914 603 41 0 11090 0
vsize: 44524
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10507 0 0 0 12959 42 0 0 25 0 1 0 480502418 45592576 9916 4294967295 134512640 134672761 3221224560 3221223152 134607812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 9916 603 41 0 11090 0
vsize: 44524
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10509 0 0 0 13959 42 0 0 25 0 1 0 480502418 45592576 9918 4294967295 134512640 134672761 3221224560 3221222624 134566692 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 9918 603 41 0 11090 0
vsize: 44524
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10510 0 0 0 14959 42 0 0 25 0 1 0 480502418 45592576 9919 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 9919 603 41 0 11090 0
vsize: 44524
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10512 0 0 0 15960 42 0 0 25 0 1 0 480502418 45592576 9921 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 9921 603 41 0 11090 0
vsize: 44524
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10530 0 0 0 16960 42 0 0 25 0 1 0 480502418 45821952 9939 4294967295 134512640 134672761 3221224560 3221223088 134606423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 9939 603 41 0 11146 0
vsize: 44748
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10533 0 0 0 17960 42 0 0 25 0 1 0 480502418 45821952 9942 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 9942 603 41 0 11146 0
vsize: 44748
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10536 0 0 0 18960 42 0 0 25 0 1 0 480502418 45821952 9945 4294967295 134512640 134672761 3221224560 3221222864 134566556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 9945 603 41 0 11146 0
vsize: 44748
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10542 0 0 0 19960 42 0 0 25 0 1 0 480502418 45821952 9951 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 9951 603 41 0 11146 0
vsize: 44748
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10544 0 0 0 20960 42 0 0 25 0 1 0 480502418 45821952 9953 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 9953 603 41 0 11146 0
vsize: 44748
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10544 0 0 0 21960 42 0 0 25 0 1 0 480502418 45821952 9953 4294967295 134512640 134672761 3221224560 3221223008 134643951 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 9953 603 41 0 11146 0
vsize: 44748
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10876 0 0 0 22959 43 0 0 25 0 1 0 480502418 48295936 10285 4294967295 134512640 134672761 3221224560 3221223024 134644251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11791 10285 603 41 0 11750 0
vsize: 47164
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10876 0 0 0 23960 43 0 0 25 0 1 0 480502418 48295936 10285 4294967295 134512640 134672761 3221224560 3221223056 134606964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11791 10285 603 41 0 11750 0
vsize: 47164
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10876 0 0 0 24960 43 0 0 25 0 1 0 480502418 48295936 10285 4294967295 134512640 134672761 3221224560 3221222732 134642912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11791 10285 603 41 0 11750 0
vsize: 47164
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10876 0 0 0 25960 43 0 0 25 0 1 0 480502418 45821952 9953 4294967295 134512640 134672761 3221224560 3221222768 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 9953 603 41 0 11146 0
vsize: 44748
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10876 0 0 0 26960 43 0 0 25 0 1 0 480502418 45821952 9953 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 9953 603 41 0 11146 0
vsize: 44748
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 10960 0 0 0 27960 43 0 0 25 0 1 0 480502418 46067712 10037 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11247 10037 603 41 0 11206 0
vsize: 44988
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 11647 0 0 0 28959 44 0 0 25 0 1 0 480502418 48844800 10724 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11925 10724 603 41 0 11884 0
vsize: 47700
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14433 0 0 0 29948 56 0 0 25 0 1 0 480502418 60469248 12224 4294967295 134512640 134672761 3221224560 3221223104 134621104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14763 12224 603 41 0 14722 0
vsize: 59052
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14433 0 0 0 30920 84 0 0 25 0 1 0 480502418 57831424 11892 4294967295 134512640 134672761 3221224560 3221222768 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14119 11892 603 41 0 14078 0
vsize: 56476
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14433 0 0 0 31793 133 0 0 25 0 1 0 480502418 57831424 11892 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14119 11892 603 41 0 14078 0
vsize: 56476
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14433 0 0 0 32793 133 0 0 25 0 1 0 480502418 57831424 11892 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14119 11892 603 41 0 14078 0
vsize: 56476
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14433 0 0 0 33793 133 0 0 25 0 1 0 480502418 57831424 11892 4294967295 134512640 134672761 3221224560 3221222800 1075349639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14119 11892 603 41 0 14078 0
vsize: 56476
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14765 0 0 0 34793 134 0 0 25 0 1 0 480502418 60469248 12224 4294967295 134512640 134672761 3221224560 3221223272 134643244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14763 12224 603 41 0 14722 0
vsize: 59052
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14765 0 0 0 35792 134 0 0 25 0 1 0 480502418 60469248 12224 4294967295 134512640 134672761 3221224560 3221223104 134621219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14763 12224 603 41 0 14722 0
vsize: 59052
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14765 0 0 0 36792 134 0 0 25 0 1 0 480502418 57831424 11892 4294967295 134512640 134672761 3221224560 3221223072 134638292 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14119 11892 603 41 0 14078 0
vsize: 56476
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14765 0 0 0 37792 134 0 0 25 0 1 0 480502418 57831424 11892 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14119 11892 603 41 0 14078 0
vsize: 56476
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 14994 0 0 0 38792 135 0 0 25 0 1 0 480502418 58863616 12121 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14371 12121 603 41 0 14330 0
vsize: 57484
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 15499 0 0 0 39791 136 0 0 25 0 1 0 480502418 60964864 12626 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14884 12626 603 41 0 14843 0
vsize: 59536
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 16032 0 0 0 40789 138 0 0 25 0 1 0 480502418 63041536 13159 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15391 13159 603 41 0 15350 0
vsize: 61564
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 16634 0 0 0 41787 140 0 0 25 0 1 0 480502418 65572864 13761 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16009 13761 603 41 0 15968 0
vsize: 64036
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 17154 0 0 0 42785 142 0 0 25 0 1 0 480502418 67678208 14281 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16523 14281 603 41 0 16482 0
vsize: 66092
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 17642 0 0 0 43785 143 0 0 25 0 1 0 480502418 69754880 14769 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17030 14769 603 41 0 16989 0
vsize: 68120
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 18249 0 0 0 44783 145 0 0 25 0 1 0 480502418 72212480 15376 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17630 15376 603 41 0 17589 0
vsize: 70520
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 18794 0 0 0 45781 147 0 0 25 0 1 0 480502418 74444800 15921 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 15921 603 41 0 18134 0
vsize: 72700
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 19489 0 0 0 46780 148 0 0 25 0 1 0 480502418 77197312 16616 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18847 16616 603 41 0 18806 0
vsize: 75388
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 19991 0 0 0 47779 150 0 0 25 0 1 0 480502418 79298560 17118 4294967295 134512640 134672761 3221224560 3221223704 134616154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19360 17118 603 41 0 19319 0
vsize: 77440
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 20348 0 0 0 48778 151 0 0 25 0 1 0 480502418 80728064 17475 4294967295 134512640 134672761 3221224560 3221223744 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19709 17475 603 41 0 19668 0
vsize: 78836
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 20868 0 0 0 49776 152 0 0 25 0 1 0 480502418 82821120 17995 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17995 603 41 0 20179 0
vsize: 80880
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 21440 0 0 0 50775 154 0 0 25 0 1 0 480502418 85291008 18567 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20823 18567 603 41 0 20782 0
vsize: 83292
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 24044 0 0 0 51753 175 0 0 25 0 1 0 480502418 88543232 19110 4294967295 134512640 134672761 3221224560 3221223052 134642869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21617 19110 603 41 0 21576 0
vsize: 86468
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 24044 0 0 0 52743 186 0 0 25 0 1 0 480502418 85905408 18778 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20973 18778 603 41 0 20932 0
vsize: 83892
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 24044 0 0 0 53743 186 0 0 25 0 1 0 480502418 85905408 18778 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20973 18778 603 41 0 20932 0
vsize: 83892
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 24046 0 0 0 54743 186 0 0 25 0 1 0 480502418 85905408 18780 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20973 18780 603 41 0 20932 0
vsize: 83892
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 24377 0 0 0 55743 187 0 0 25 0 1 0 480502418 87314432 19111 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21317 19111 603 41 0 21276 0
vsize: 85268
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 24855 0 0 0 56742 188 0 0 25 0 1 0 480502418 89276416 19589 4294967295 134512640 134672761 3221224560 3221223704 134616320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21796 19589 603 41 0 21755 0
vsize: 87184
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 25333 0 0 0 57741 189 0 0 25 0 1 0 480502418 91209728 20068 4294967295 134512640 134672761 3221224560 3221223568 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22268 20068 603 41 0 22227 0
vsize: 89072
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 26158 0 0 0 58740 190 0 0 25 0 1 0 480502418 94654464 20892 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23109 20892 603 41 0 23068 0
vsize: 92436
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 26781 0 0 0 59738 192 0 0 25 0 1 0 480502418 97132544 21515 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 21515 603 41 0 23673 0
vsize: 94856
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 27250 0 0 0 60737 194 0 0 25 0 1 0 480502418 99069952 21984 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24187 21984 603 41 0 24146 0
vsize: 96748
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 27602 0 0 0 61736 194 0 0 25 0 1 0 480502418 100507648 22336 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24538 22336 603 41 0 24497 0
vsize: 98152
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 28079 0 0 0 62736 195 0 0 25 0 1 0 480502418 102404096 22813 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25001 22813 603 41 0 24960 0
vsize: 100004
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 28534 0 0 0 63734 197 0 0 25 0 1 0 480502418 104329216 23268 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 23268 603 41 0 25430 0
vsize: 101884
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 28900 0 0 0 64734 197 0 0 25 0 1 0 480502418 105746432 23634 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25817 23634 603 41 0 25776 0
vsize: 103268
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 29269 0 0 0 65733 198 0 0 25 0 1 0 480502418 107331584 24003 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26204 24003 603 41 0 26163 0
vsize: 104816
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 29916 0 0 0 66732 199 0 0 25 0 1 0 480502418 109883392 24650 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26827 24650 603 41 0 26786 0
vsize: 107308
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 30349 0 0 0 67731 200 0 0 25 0 1 0 480502418 111697920 25083 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27270 25083 603 41 0 27229 0
vsize: 109080
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 30863 0 0 0 68730 201 0 0 25 0 1 0 480502418 113758208 25597 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27773 25597 603 41 0 27732 0
vsize: 111092
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 31187 0 0 0 69730 202 0 0 25 0 1 0 480502418 115064832 25921 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28092 25921 603 41 0 28051 0
vsize: 112368
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 31610 0 0 0 70729 203 0 0 25 0 1 0 480502418 116850688 26344 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28528 26344 603 41 0 28487 0
vsize: 114112
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 32092 0 0 0 71728 204 0 0 25 0 1 0 480502418 118829056 26826 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29011 26826 603 41 0 28970 0
vsize: 116044
[startup+730.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 32425 0 0 0 72726 206 0 0 25 0 1 0 480502418 120131584 27159 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29329 27159 603 41 0 29288 0
vsize: 117316
[startup+740.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 32693 0 0 0 73725 206 0 0 25 0 1 0 480502418 121315328 27427 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29618 27427 603 41 0 29577 0
vsize: 118472
[startup+750.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 33046 0 0 0 74725 207 0 0 25 0 1 0 480502418 122740736 27780 4294967295 134512640 134672761 3221224560 3221223568 134607908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29966 27780 603 41 0 29925 0
vsize: 119864
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 33439 0 0 0 75724 208 0 0 25 0 1 0 480502418 124305408 28173 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30348 28173 603 41 0 30307 0
vsize: 121392
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 33957 0 0 0 76723 208 0 0 25 0 1 0 480502418 126402560 28691 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30860 28691 603 41 0 30819 0
vsize: 123440
[startup+780.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 34302 0 0 0 77723 209 0 0 25 0 1 0 480502418 128098304 29036 4294967295 134512640 134672761 3221224560 3221223704 134616373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31274 29036 603 41 0 31233 0
vsize: 125096
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 34778 0 0 0 78722 211 0 0 25 0 1 0 480502418 130027520 29512 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31745 29512 603 41 0 31704 0
vsize: 126980
[startup+800.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 35222 0 0 0 79721 212 0 0 25 0 1 0 480502418 131833856 29956 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32186 29956 603 41 0 32145 0
vsize: 128744
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 35625 0 0 0 80720 213 0 0 25 0 1 0 480502418 133529600 30359 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32600 30359 603 41 0 32559 0
vsize: 130400
[startup+820.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 36039 0 0 0 81720 213 0 0 25 0 1 0 480502418 135213056 30773 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33011 30773 603 41 0 32970 0
vsize: 132044
[startup+830.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 36488 0 0 0 82719 214 0 0 25 0 1 0 480502418 137015296 31222 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33451 31222 603 41 0 33410 0
vsize: 133804
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 37006 0 0 0 83718 215 0 0 25 0 1 0 480502418 139173888 31740 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33978 31740 603 41 0 33937 0
vsize: 135912
[startup+850.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 37436 0 0 0 84717 216 0 0 25 0 1 0 480502418 140873728 32170 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34393 32170 603 41 0 34352 0
vsize: 137572
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 37825 0 0 0 85716 217 0 0 25 0 1 0 480502418 142446592 32559 4294967295 134512640 134672761 3221224560 3221223424 1075349719 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34777 32559 603 41 0 34736 0
vsize: 139108
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 38271 0 0 0 86715 218 0 0 25 0 1 0 480502418 144371712 33005 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35247 33005 603 41 0 35206 0
vsize: 140988
[startup+880.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 38700 0 0 0 87714 219 0 0 25 0 1 0 480502418 146051072 33434 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35657 33434 603 41 0 35616 0
vsize: 142628
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 39403 0 0 0 88713 221 0 0 25 0 1 0 480502418 148901888 34137 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36353 34137 603 41 0 36312 0
vsize: 145412
[startup+900.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 39763 0 0 0 89712 222 0 0 25 0 1 0 480502418 150450176 34497 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36731 34497 603 41 0 36690 0
vsize: 146924
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 40200 0 0 0 90711 223 0 0 25 0 1 0 480502418 152268800 34934 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37175 34934 603 41 0 37134 0
vsize: 148700
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 40540 0 0 0 91710 225 0 0 25 0 1 0 480502418 153567232 35274 4294967295 134512640 134672761 3221224560 3221223760 134610688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37492 35274 603 41 0 37451 0
vsize: 149968
[startup+930.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 40970 0 0 0 92709 226 0 0 25 0 1 0 480502418 155389952 35704 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37937 35704 603 41 0 37896 0
vsize: 151748
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 41327 0 0 0 93708 227 0 0 25 0 1 0 480502418 156835840 36061 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38290 36061 603 41 0 38249 0
vsize: 153160
[startup+950.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 41514 0 0 0 94708 227 0 0 25 0 1 0 480502418 157622272 36248 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38482 36248 603 41 0 38441 0
vsize: 153928
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 42061 0 0 0 95706 229 0 0 25 0 1 0 480502418 159817728 36795 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39018 36795 603 41 0 38977 0
vsize: 156072
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 42564 0 0 0 96705 230 0 0 25 0 1 0 480502418 161816576 37298 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39506 37298 603 41 0 39465 0
vsize: 158024
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 43107 0 0 0 97703 232 0 0 25 0 1 0 480502418 164143104 37841 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40074 37841 603 41 0 40033 0
vsize: 160296
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 43482 0 0 0 98703 233 0 0 25 0 1 0 480502418 165564416 38216 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40421 38216 603 41 0 40380 0
vsize: 161684
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 43743 0 0 0 99702 234 0 0 25 0 1 0 480502418 166621184 38477 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40679 38477 603 41 0 40638 0
vsize: 162716
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 44371 0 0 0 100701 235 0 0 25 0 1 0 480502418 169205760 39105 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41310 39105 603 41 0 41269 0
vsize: 165240
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 44575 0 0 0 101700 236 0 0 25 0 1 0 480502418 170119168 39309 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41533 39309 603 41 0 41492 0
vsize: 166132
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 44917 0 0 0 102700 237 0 0 25 0 1 0 480502418 171532288 39651 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41878 39651 603 41 0 41837 0
vsize: 167512
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 45723 0 0 0 103698 239 0 0 25 0 1 0 480502418 174747648 40457 4294967295 134512640 134672761 3221224560 3221223600 134614207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42663 40457 603 41 0 42622 0
vsize: 170652
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 46016 0 0 0 104697 240 0 0 25 0 1 0 480502418 175910912 40750 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42947 40750 603 41 0 42906 0
vsize: 171788
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 46297 0 0 0 105697 240 0 0 25 0 1 0 480502418 177098752 41031 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43237 41031 603 41 0 43196 0
vsize: 172948
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 46615 0 0 0 106696 241 0 0 25 0 1 0 480502418 178417664 41349 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43559 41349 603 41 0 43518 0
vsize: 174236
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 47155 0 0 0 107695 243 0 0 25 0 1 0 480502418 180592640 41889 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44090 41889 603 41 0 44049 0
vsize: 176360
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 47794 0 0 0 108694 244 0 0 25 0 1 0 480502418 183218176 42528 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44731 42528 603 41 0 44690 0
vsize: 178924
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 48309 0 0 0 109693 245 0 0 25 0 1 0 480502418 185290752 43043 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45237 43043 603 41 0 45196 0
vsize: 180948
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 48626 0 0 0 110692 246 0 0 25 0 1 0 480502418 186576896 43360 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45551 43360 603 41 0 45510 0
vsize: 182204
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 48910 0 0 0 111692 247 0 0 25 0 1 0 480502418 187748352 43644 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45837 43644 603 41 0 45796 0
vsize: 183348
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 49443 0 0 0 112690 248 0 0 25 0 1 0 480502418 189956096 44177 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46376 44177 603 41 0 46335 0
vsize: 185504
[startup+1140.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 50098 0 0 0 113689 250 0 0 25 0 1 0 480502418 192638976 44832 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47031 44832 603 41 0 46990 0
vsize: 188124
[startup+1150.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 50993 0 0 0 114686 253 0 0 25 0 1 0 480502418 196268032 45727 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47917 45727 603 41 0 47876 0
vsize: 191668
[startup+1160.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 51811 0 0 0 115684 255 0 0 25 0 1 0 480502418 199643136 46545 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48741 46545 603 41 0 48700 0
vsize: 194964
[startup+1170.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 52477 0 0 0 116682 257 0 0 25 0 1 0 480502418 202375168 47211 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49408 47211 603 41 0 49367 0
vsize: 197632
[startup+1180.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 52725 0 0 0 117682 258 0 0 25 0 1 0 480502418 203407360 47459 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49660 47459 603 41 0 49619 0
vsize: 198640
[startup+1190.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 53088 0 0 0 118681 259 0 0 25 0 1 0 480502418 204931072 47822 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50032 47822 603 41 0 49991 0
vsize: 200128
[startup+1200.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 53510 0 0 0 119680 260 0 0 25 0 1 0 480502418 206635008 48244 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50448 48244 603 41 0 50407 0
vsize: 201792
[startup+1210.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2138
Raw data (stat): 2138 (minisat+) R 2137 28546 28545 0 -1 0 53804 0 0 0 120679 261 0 0 25 0 1 0 480502418 207818752 48538 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50737 48538 603 41 0 50696 0
vsize: 202948
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.16 s]
Raw data (loadavg): 1.02 0.99 0.91 1/54 2138
Raw data (stat): 2138 (minisat+) Z 2137 28546 28545 0 -1 12 53805 0 0 0 120679 275 0 0 25 0 1 0 480502418 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.16
CPU time (s): 1209.56
CPU user time (s): 1206.8
CPU system time (s): 2.75658
CPU usage (%): 99.95
Max. virtual memory (Kb): 202948
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####