PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-4.opb
MD5SUM	b85a90571dde4fe12541342d5605d680
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-37
Optimality of the best value was proved	NO
Number of terms in the objective function	1150
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1150
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1150
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.1
Number of variables	1150
Total number of constraints	80258
Number of constraints which are clauses	80258
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 6009

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        817976 kB
Buffers:         35968 kB
Cached:         145460 kB
SwapCached:       2376 kB
Active:          60700 kB
Inactive:       126124 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        817724 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            24112 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:15:12 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4473 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80258 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   80258   160516 |   26752       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  148144   319772 |   49381       0        0     nan |  0.000 % |
c |       100 |  147820   319103 |   54319      84      567     6.8 |  0.388 % |
c |       250 |  147145   317664 |   59751     188     1432     7.6 |  1.214 % |
c |       476 |  146024   315267 |   65726     361     3068     8.5 |  2.595 % |
c |       813 |  143729   310234 |   72298     619     5841     9.4 |  5.557 % |
c |      1319 |  140833   303816 |   79528     968     9121     9.4 |  9.437 % |
c |      2079 |  136692   294527 |   87481    1586    15869    10.0 | 15.004 % |
c |      3218 |  131314   282313 |   96229    2417    27902    11.5 | 22.323 % |
c |      4926 |  122752   262701 |  105852    3528    39936    11.3 | 34.222 % |
c |      7488 |  112044   237857 |  116437    5289    62605    11.8 | 49.090 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7928 |  111198   235994 |   37066    5633    66805    11.9 | 49.090 % |
c |      8028 |  110897   235287 |   40772    5710    67536    11.8 | 50.901 % |
c |      8178 |  110452   234225 |   44849    5792    68387    11.8 | 51.548 % |
c |      8403 |  109585   232234 |   49334    5952    71118    11.9 | 52.759 % |
c |      8741 |  108728   230226 |   54268    6208    74433    12.0 | 53.995 % |
c |      9247 |  107763   227961 |   59695    6556    79030    12.1 | 55.393 % |
c |     10006 |  106198   224277 |   65664    7058    87476    12.4 | 57.665 % |
c |     11146 |  103552   218006 |   72231    7914   103965    13.1 | 61.514 % |
c |     12854 |  100400   210497 |   79454    9088   124554    13.7 | 66.138 % |
c |     15416 |   97019   202392 |   87399   10804   161729    15.0 | 71.090 % |
c |     19260 |   94852   197144 |   96139   14054   253306    18.0 | 74.363 % |
c |     25026 |   93592   194098 |  105753   19178   576284    30.0 | 76.268 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29121 |   92780   192183 |   30926   22895   940622    41.1 | 76.268 % |
c |     29221 |   92677   191930 |   34018   22961   941837    41.0 | 77.647 % |
c |     29371 |   92612   191776 |   37420   23105   945249    40.9 | 77.742 % |
c |     29597 |   92612   191776 |   41162   23331   954744    40.9 | 77.742 % |
c |     29934 |   92495   191494 |   45278   23662   962311    40.7 | 77.917 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30329 |   92131   190575 |   30710   23891   984433    41.2 | 77.917 % |
c |     30429 |   92064   190426 |   33781   23974   986115    41.1 | 78.509 % |
c |     30579 |   91949   190146 |   37159   24115   994438    41.2 | 78.683 % |
c |     30804 |   91850   189911 |   40875   24280  1003798    41.3 | 78.828 % |
c |     31141 |   91766   189701 |   44962   24546  1013462    41.3 | 78.962 % |
c |     31647 |   91650   189414 |   49458   25021  1032977    41.3 | 79.143 % |
c |     32406 |   91601   189300 |   54404   25733  1089814    42.4 | 79.212 % |
c |     33545 |   91498   189059 |   59845   26813  1189985    44.4 | 79.358 % |
c |     35253 |   91064   187999 |   65829   28271  1265964    44.8 | 80.005 % |
c |     37817 |   90592   186879 |   72412   30523  1417125    46.4 | 80.691 % |
c |     41661 |   90247   186028 |   79653   34043  1688146    49.6 | 81.219 % |
c |     47427 |   89873   185101 |   87619   39490  2309222    58.5 | 81.806 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55522 |   89822   185003 |   29940   47545  3314007    69.7 | 81.806 % |
c |     55622 |   89822   185003 |   32934   47645  3321718    69.7 | 81.930 % |
c |     55772 |   89822   185003 |   36227   47795  3326427    69.6 | 81.931 % |
c |     55998 |   89822   185003 |   39850   48021  3341366    69.6 | 81.930 % |
c |     56336 |   89822   185003 |   43835   48359  3370021    69.7 | 81.931 % |
c |     56842 |   89822   185003 |   48218   48865  3409651    69.8 | 81.930 % |
c |     57601 |   89177   183450 |   53040   48863  3434237    70.3 | 82.894 % |
c |     58740 |   89177   183450 |   58344   50002  3579676    71.6 | 82.894 % |
c |     60448 |   89117   183296 |   64179   51669  3732132    72.2 | 82.996 % |
c |     63011 |   89039   183106 |   70596   54124  3965144    73.3 | 83.114 % |
c |     66855 |   89039   183106 |   77656   57968  4599226    79.3 | 83.114 % |
c |     72622 |   88752   182402 |   85422   63069  5112366    81.1 | 83.557 % |
c |     81271 |   88748   182392 |   93964   71717  6426102    89.6 | 83.564 % |
c |     94245 |   88748   182392 |  103361   84691  8009047    94.6 | 83.564 % |
c |    113707 |   88741   182375 |  113697  104135 11319413   108.7 | 83.574 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    140871 |   88488   181720 |   29496  130980 15028721   114.7 | 83.574 % |
c |    140971 |   88488   181720 |   32445   23657  1604034    67.8 | 83.975 % |
c |    141121 |   88488   181720 |   35690   23807  1613264    67.8 | 83.975 % |
c |    141346 |   88488   181720 |   39259   24032  1631251    67.9 | 83.975 % |
c |    141683 |   88328   181322 |   43185   24359  1642586    67.4 | 84.221 % |
c |    142189 |   88328   181322 |   47503   24865  1700627    68.4 | 84.221 % |
c |    142948 |   88328   181322 |   52253   25624  1787151    69.7 | 84.221 % |
c |    144087 |   88328   181322 |   57479   26763  1947089    72.8 | 84.221 % |
c |    145797 |   88226   181078 |   63227   28458  2159705    75.9 | 84.369 % |
c |    148359 |   88221   181067 |   69550   31016  2379812    76.7 | 84.375 % |
c |    152203 |   88221   181067 |   76505   34860  2924276    83.9 | 84.375 % |
c |    157969 |   88221   181067 |   84155   40626  3769186    92.8 | 84.375 % |
c |    166618 |   88180   180970 |   92571   49077  4992109   101.7 | 84.436 % |
c |    179592 |   88139   180873 |  101828   61925  6663510   107.6 | 84.496 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    193053 |   88160   180935 |   29386   75386  9039640   119.9 | 84.496 % |
c |    193153 |   88154   180921 |   32324   20076  2226072   110.9 | 84.484 % |
c |    193303 |   88149   180908 |   35557   20222  2233119   110.4 | 84.492 % |
c |    193528 |   88149   180908 |   39112   20447  2240695   109.6 | 84.492 % |
c |    193865 |   87960   180457 |   43024   20704  2251356   108.7 | 84.765 % |
c |    194373 |   87960   180457 |   47326   21212  2285864   107.8 | 84.765 % |
c |    195133 |   87928   180387 |   52059   21969  2317828   105.5 | 84.806 % |
c |    196272 |   87928   180387 |   57265   23108  2390481   103.4 | 84.806 % |
c |    197981 |   87877   180262 |   62991   24808  2557155   103.1 | 84.886 % |
c |    200543 |   87877   180262 |   69290   27370  2839758   103.8 | 84.886 % |
c |    204387 |   87859   180218 |   76219   31206  3310018   106.1 | 84.914 % |
c |    210154 |   87728   179913 |   83841   36956  3914827   105.9 | 85.101 % |
c |    218803 |   87618   179642 |   92225   45444  4968749   109.3 | 85.273 % |
c |    231778 |   87612   179628 |  101448   58416  6873546   117.7 | 85.281 % |
c |    251240 |   87602   179602 |  111593   77876  9366492   120.3 | 85.299 % |
c |    280433 |   87500   179360 |  122752  106975 13247285   123.8 | 85.449 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 C4#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.99 0.97 0.91 2/55 28088
Raw data (stat): 28088 (runsolver) R 28087 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481160121 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28088
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 4909 0 0 0 984 14 0 0 25 0 1 0 481160121 23216128 4887 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5668 4887 603 41 0 5627 0
vsize: 22672
[startup+20.0016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28088
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 4917 0 0 0 1984 14 0 0 25 0 1 0 481160121 23216128 4895 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5668 4895 603 41 0 5627 0
vsize: 22672
[startup+30.0018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 4931 0 0 0 2983 15 0 0 25 0 1 0 481160121 23216128 4909 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5668 4909 603 41 0 5627 0
vsize: 22672
[startup+40.0017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 4937 0 0 0 3982 15 0 0 25 0 1 0 481160121 23351296 4915 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5701 4915 603 41 0 5660 0
vsize: 22804
[startup+50.0014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 4949 0 0 0 4982 15 0 0 25 0 1 0 481160121 23351296 4927 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5701 4927 603 41 0 5660 0
vsize: 22804
[startup+60.0016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 4958 0 0 0 5982 16 0 0 25 0 1 0 481160121 23351296 4936 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5701 4936 603 41 0 5660 0
vsize: 22804
[startup+70.0015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 5088 0 0 0 6981 16 0 0 25 0 1 0 481160121 24240128 5066 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5918 5066 603 41 0 5877 0
vsize: 23672
[startup+80.0022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 5088 0 0 0 7981 16 0 0 25 0 1 0 481160121 24240128 5066 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5918 5066 603 41 0 5877 0
vsize: 23672
[startup+90.0024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 5156 0 0 0 8981 17 0 0 25 0 1 0 481160121 24510464 5134 4294967295 134512640 134672761 3221224560 3221223808 134562289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5984 5134 603 41 0 5943 0
vsize: 23936
[startup+100.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 5465 0 0 0 9980 18 0 0 25 0 1 0 481160121 25784320 5443 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6295 5443 603 41 0 6254 0
vsize: 25180
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 5990 0 0 0 10978 19 0 0 25 0 1 0 481160121 27922432 5968 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6817 5968 603 41 0 6776 0
vsize: 27268
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 6274 0 0 0 11978 20 0 0 25 0 1 0 481160121 29130752 6252 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7112 6252 603 41 0 7071 0
vsize: 28448
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 6591 0 0 0 12977 21 0 0 25 0 1 0 481160121 30470144 6569 4294967295 134512640 134672761 3221224560 3221223744 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7439 6569 603 41 0 7398 0
vsize: 29756
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 7021 0 0 0 13976 23 0 0 25 0 1 0 481160121 32337920 6999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7895 6999 603 41 0 7854 0
vsize: 31580
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 7510 0 0 0 14975 24 0 0 25 0 1 0 481160121 34222080 7488 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8355 7488 603 41 0 8314 0
vsize: 33420
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 8017 0 0 0 15974 25 0 0 25 0 1 0 481160121 36376576 7995 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8881 7995 603 41 0 8840 0
vsize: 35524
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 8556 0 0 0 16972 27 0 0 25 0 1 0 481160121 38514688 8534 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9403 8534 603 41 0 9362 0
vsize: 37612
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 8772 0 0 0 17971 28 0 0 25 0 1 0 481160121 39411712 8750 4294967295 134512640 134672761 3221224560 3221223616 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9622 8750 603 41 0 9581 0
vsize: 38488
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 9158 0 0 0 18970 29 0 0 25 0 1 0 481160121 41025536 9136 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10016 9136 603 41 0 9975 0
vsize: 40064
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 9732 0 0 0 19968 31 0 0 25 0 1 0 481160121 43311104 9710 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10574 9710 603 41 0 10533 0
vsize: 42296
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 10084 0 0 0 20967 33 0 0 25 0 1 0 481160121 44793856 10062 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10936 10062 603 41 0 10895 0
vsize: 43744
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 10431 0 0 0 21965 34 0 0 25 0 1 0 481160121 46129152 10409 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11262 10409 603 41 0 11221 0
vsize: 45048
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 10955 0 0 0 22964 36 0 0 25 0 1 0 481160121 48263168 10933 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11783 10933 603 41 0 11742 0
vsize: 47132
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 11424 0 0 0 23961 38 0 0 25 0 1 0 481160121 50393088 11402 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12303 11402 603 41 0 12262 0
vsize: 49212
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 11864 0 0 0 24960 40 0 0 25 0 1 0 481160121 52260864 11842 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12759 11842 603 41 0 12718 0
vsize: 51036
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 12296 0 0 0 25958 42 0 0 25 0 1 0 481160121 53993472 12274 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13182 12274 603 41 0 13141 0
vsize: 52728
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 12660 0 0 0 26957 43 0 0 25 0 1 0 481160121 55459840 12638 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13540 12638 603 41 0 13499 0
vsize: 54160
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 13007 0 0 0 27955 45 0 0 25 0 1 0 481160121 56942592 12985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13902 12985 603 41 0 13861 0
vsize: 55608
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28090
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 13413 0 0 0 28955 46 0 0 25 0 1 0 481160121 58556416 13391 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14296 13391 603 41 0 14255 0
vsize: 57184
[startup+300.01 s]
Raw data (loadavg): 1.07 0.99 0.91 4/60 28142
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 13779 0 0 0 29953 47 0 0 25 0 1 0 481160121 60018688 13757 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14653 13757 603 41 0 14612 0
vsize: 58612
[startup+310.011 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 28143
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 14124 0 0 0 30952 48 0 0 25 0 1 0 481160121 61493248 14102 4294967295 134512640 134672761 3221224560 3221223488 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15013 14102 603 41 0 14972 0
vsize: 60052
[startup+320.011 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 28143
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 14525 0 0 0 31951 49 0 0 25 0 1 0 481160121 63098880 14503 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15405 14503 603 41 0 15364 0
vsize: 61620
[startup+330.011 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 28145
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 14902 0 0 0 32950 51 0 0 25 0 1 0 481160121 64569344 14880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15764 14880 603 41 0 15723 0
vsize: 63056
[startup+340.011 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 28145
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 15274 0 0 0 33949 52 0 0 25 0 1 0 481160121 66162688 15252 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16153 15252 603 41 0 16112 0
vsize: 64612
[startup+350.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 28145
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 15681 0 0 0 34947 54 0 0 25 0 1 0 481160121 67756032 15659 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16542 15659 603 41 0 16501 0
vsize: 66168
[startup+360.011 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 28145
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 16093 0 0 0 35947 55 0 0 25 0 1 0 481160121 69488640 16071 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16965 16071 603 41 0 16924 0
vsize: 67860
[startup+370.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 28145
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 16476 0 0 0 36946 55 0 0 25 0 1 0 481160121 71077888 16454 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17353 16454 603 41 0 17312 0
vsize: 69412
[startup+380.011 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 16856 0 0 0 37945 57 0 0 25 0 1 0 481160121 72536064 16834 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17709 16834 603 41 0 17668 0
vsize: 70836
[startup+390.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 17178 0 0 0 38944 58 0 0 25 0 1 0 481160121 73863168 17156 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18033 17156 603 41 0 17992 0
vsize: 72132
[startup+400.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 17493 0 0 0 39943 59 0 0 25 0 1 0 481160121 75194368 17471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18358 17471 603 41 0 18317 0
vsize: 73432
[startup+410.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 17823 0 0 0 40942 61 0 0 25 0 1 0 481160121 76529664 17801 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18684 17801 603 41 0 18643 0
vsize: 74736
[startup+420.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 18202 0 0 0 41941 61 0 0 25 0 1 0 481160121 77996032 18180 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19042 18180 603 41 0 19001 0
vsize: 76168
[startup+430.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 18574 0 0 0 42941 62 0 0 25 0 1 0 481160121 79601664 18552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19434 18552 603 41 0 19393 0
vsize: 77736
[startup+440.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 18966 0 0 0 43940 63 0 0 25 0 1 0 481160121 81203200 18944 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19825 18944 603 41 0 19784 0
vsize: 79300
[startup+450.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 19332 0 0 0 44939 64 0 0 25 0 1 0 481160121 82681856 19310 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20186 19310 603 41 0 20145 0
vsize: 80744
[startup+460.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 19538 0 0 0 45939 64 0 0 25 0 1 0 481160121 83480576 19516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20381 19516 603 41 0 20340 0
vsize: 81524
[startup+470.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 19800 0 0 0 46938 65 0 0 25 0 1 0 481160121 84549632 19778 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20642 19778 603 41 0 20601 0
vsize: 82568
[startup+480.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 20071 0 0 0 47937 66 0 0 25 0 1 0 481160121 85618688 20049 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20903 20049 603 41 0 20862 0
vsize: 83612
[startup+490.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 20327 0 0 0 48936 67 0 0 25 0 1 0 481160121 86679552 20305 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21162 20305 603 41 0 21121 0
vsize: 84648
[startup+500.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 20586 0 0 0 49936 68 0 0 25 0 1 0 481160121 87740416 20564 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21421 20564 603 41 0 21380 0
vsize: 85684
[startup+510.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 20757 0 0 0 50936 68 0 0 25 0 1 0 481160121 88412160 20735 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21585 20735 603 41 0 21544 0
vsize: 86340
[startup+520.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21014 0 0 0 51935 69 0 0 25 0 1 0 481160121 89473024 20992 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21844 20992 603 41 0 21803 0
vsize: 87376
[startup+530.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 52935 69 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+540.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 53935 69 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+550.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 54935 69 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+560.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 55935 69 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+570.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 56935 69 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+580.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 57935 69 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+590.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 58935 69 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+600.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 59936 69 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+610.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 60936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+620.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28147
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 61936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+630.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28149
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 62936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+640.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 63936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223760 134557967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+650.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 64936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+660.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 65936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+670.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 66936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+680.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 67936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+690.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 68936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+700.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 69936 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+710.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 70937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+720.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 71937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+730.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 72937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+740.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 73937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+750.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 74937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+760.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 75937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+770.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 76937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+780.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 77937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+790.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 78937 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+800.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 79938 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+810.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 80938 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+820.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 81938 70 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+830.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 82938 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+840.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 83938 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+850.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 84938 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+860.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 85938 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+870.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 86938 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+880.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 87939 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+890.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 88939 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+900.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 89939 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+910.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 90939 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+920.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28151
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 91939 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+930.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 92939 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+940.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 93940 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+950.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 94940 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+960.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 95940 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223664 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+970.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 96940 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+980.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 97940 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+990.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21091 0 0 0 98940 71 0 0 25 0 1 0 481160121 89800704 21069 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21069 603 41 0 21883 0
vsize: 87696
[startup+1000 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21092 0 0 0 99940 71 0 0 25 0 1 0 481160121 89800704 21070 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21070 603 41 0 21883 0
vsize: 87696
[startup+1010 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21092 0 0 0 100940 71 0 0 25 0 1 0 481160121 89800704 21070 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21070 603 41 0 21883 0
vsize: 87696
[startup+1020 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21093 0 0 0 101940 72 0 0 25 0 1 0 481160121 89800704 21071 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21071 603 41 0 21883 0
vsize: 87696
[startup+1030 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21093 0 0 0 102940 72 0 0 25 0 1 0 481160121 89800704 21071 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21071 603 41 0 21883 0
vsize: 87696
[startup+1040 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21093 0 0 0 103940 72 0 0 25 0 1 0 481160121 89800704 21071 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21071 603 41 0 21883 0
vsize: 87696
[startup+1050 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21102 0 0 0 104940 72 0 0 25 0 1 0 481160121 89800704 21080 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21924 21080 603 41 0 21883 0
vsize: 87696
[startup+1060 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21367 0 0 0 105940 73 0 0 25 0 1 0 481160121 91000832 21345 4294967295 134512640 134672761 3221224560 3221223664 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22217 21345 603 41 0 22176 0
vsize: 88868
[startup+1070 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21595 0 0 0 106939 73 0 0 25 0 1 0 481160121 91938816 21573 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22446 21573 603 41 0 22405 0
vsize: 89784
[startup+1080 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 21775 0 0 0 107939 74 0 0 25 0 1 0 481160121 92598272 21753 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22607 21753 603 41 0 22566 0
vsize: 90428
[startup+1090 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 22006 0 0 0 108939 74 0 0 25 0 1 0 481160121 93519872 21984 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22832 21984 603 41 0 22791 0
vsize: 91328
[startup+1100 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 22238 0 0 0 109938 75 0 0 25 0 1 0 481160121 94449664 22216 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23059 22216 603 41 0 23018 0
vsize: 92236
[startup+1110 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 22459 0 0 0 110938 75 0 0 25 0 1 0 481160121 95895552 22437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23412 22437 603 41 0 23371 0
vsize: 93648
[startup+1120 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 22679 0 0 0 111937 76 0 0 25 0 1 0 481160121 96829440 22657 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23640 22657 603 41 0 23599 0
vsize: 94560
[startup+1130 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 22889 0 0 0 112937 77 0 0 25 0 1 0 481160121 97624064 22867 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23834 22867 603 41 0 23793 0
vsize: 95336
[startup+1140 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 23090 0 0 0 113937 77 0 0 25 0 1 0 481160121 98553856 23068 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24061 23068 603 41 0 24020 0
vsize: 96244
[startup+1150 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 23267 0 0 0 114937 77 0 0 25 0 1 0 481160121 99209216 23245 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24221 23245 603 41 0 24180 0
vsize: 96884
[startup+1160 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 23460 0 0 0 115937 78 0 0 25 0 1 0 481160121 100012032 23438 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24417 23438 603 41 0 24376 0
vsize: 97668
[startup+1170 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 23643 0 0 0 116937 78 0 0 25 0 1 0 481160121 100814848 23621 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24613 23621 603 41 0 24572 0
vsize: 98452
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 23783 0 0 0 117937 78 0 0 25 0 1 0 481160121 101355520 23761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24745 23761 603 41 0 24704 0
vsize: 98980
[startup+1190 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 23997 0 0 0 118936 79 0 0 25 0 1 0 481160121 102154240 23975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24940 23975 603 41 0 24899 0
vsize: 99760
[startup+1200 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28153
Raw data (stat): 28088 (minisat+) R 28087 20838 20837 0 -1 0 24248 0 0 0 119936 79 0 0 25 0 1 0 481160121 103227392 24226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25202 24226 603 41 0 25161 0
vsize: 100808
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 28153
Raw data (stat): 28088 (minisat+) Z 28087 20838 20837 0 -1 12 24251 0 0 0 119937 84 0 0 25 0 1 0 481160121 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.22
CPU user time (s): 1199.37
CPU system time (s): 0.844871
CPU usage (%): 100.013
Max. virtual memory (Kb): 100808
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####