PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-13 22:55:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3714 boxname=wulflinc30 idbench=330 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a931f7e9a55cb6836807387327525e8b  /oldhome/oroussel/tmp/wulflinc30/normalized-frb45-21-2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc30/normalized-frb45-21-2.opb /oldhome/oroussel/tmp/wulflinc30/normalized-frb45-21-2.opb
IDLAUNCH: 3714
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        736888 kB
Buffers:         37288 kB
Cached:         219684 kB
SwapCached:          0 kB
Active:          81916 kB
Inactive:       177964 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        736636 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32300 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:15:13 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3714 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58624 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 |   58624   117248 |   19541       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1856   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71273   162476 |   23757       0        0     nan |  0.000 % |
c |       100 |   71273   162476 |   26132     100     1072    10.7 |  0.038 % |
c |       250 |   71273   162476 |   28745     250     2544    10.2 |  0.039 % |
c |       475 |   71273   162476 |   31620     475     4460     9.4 |  0.038 % |
c |       812 |   71264   162445 |   34782     810     8606    10.6 |  0.074 % |
c |      1318 |   71246   162383 |   38260    1311    13856    10.6 |  0.144 % |
c |      2077 |   71183   162166 |   42086    2054    24736    12.0 |  0.397 % |
c |      3216 |   71042   161681 |   46295    3144    37535    11.9 |  0.975 % |
c |      4924 |   70523   159904 |   50925    4715    63402    13.4 |  3.250 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 41   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5675 |   70621   160271 |   23540    5424    76265    14.1 |  3.250 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5747 |   70616   160258 |   23538    5492    76845    14.0 |  3.250 % |
c |      5847 |   70556   160050 |   25891    5577    78150    14.0 |  4.490 % |
c |      5997 |   70527   159949 |   28480    5718    81273    14.2 |  4.633 % |
c |      6222 |   70414   159564 |   31329    5916    87242    14.7 |  5.207 % |
c |      6559 |   70250   159000 |   34461    6198    93416    15.1 |  6.058 % |
c |      7067 |   70031   158245 |   37908    6649   100186    15.1 |  7.306 % |
c |      7827 |   69810   157486 |   41699    7304   116082    15.9 |  8.377 % |
c |      8966 |   69246   155550 |   45868    8268   148298    17.9 | 11.618 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 34   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9838 |   69056   154897 |   23018    9054   175958    19.4 | 11.618 % |
c |      9938 |   69006   154725 |   25319    9140   177604    19.4 | 13.146 % |
c |     10088 |   68852   154191 |   27851    9234   179949    19.5 | 14.072 % |
c |     10313 |   68776   153925 |   30636    9418   186324    19.8 | 14.535 % |
c |     10650 |   68724   153745 |   33700    9710   200915    20.7 | 14.820 % |
c |     11156 |   68146   151737 |   37070    9968   209379    21.0 | 18.280 % |
c |     11916 |   67921   150946 |   40777   10627   227628    21.4 | 19.879 % |
c |     13056 |   67437   149266 |   44855   11465   260421    22.7 | 23.015 % |
c |     14765 |   67095   148080 |   49341   12787   323736    25.3 | 25.083 % |
c |     17328 |   66954   147587 |   54275   15249   487817    32.0 | 26.078 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 35   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20482 |   66624   146432 |   22208   18056   710609    39.4 | 26.078 % |
c |     20582 |   66624   146432 |   24428   18156   714996    39.4 | 28.386 % |
c |     20732 |   66603   146361 |   26871   18294   718218    39.3 | 28.490 % |
c |     20957 |   66603   146361 |   29558   18519   731656    39.5 | 28.490 % |
c |     21295 |   66603   146361 |   32514   18857   753402    40.0 | 28.493 % |
c |     21802 |   66603   146361 |   35766   19364   771805    39.9 | 28.490 % |
c |     22561 |   66534   146118 |   39342   19997   797944    39.9 | 28.955 % |
c |     23702 |   66493   145977 |   43277   20972   850245    40.5 | 29.169 % |
c |     25411 |   66444   145806 |   47604   22491   983442    43.7 | 29.416 % |
c |     27973 |   66414   145704 |   52365   24977  1223533    49.0 | 29.561 % |
c |     31818 |   66166   144850 |   57601   28193  1461862    51.9 | 31.342 % |
c |     37584 |   66055   144457 |   63362   33870  2112369    62.4 | 32.161 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 36   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38972 |   66058   144471 |   22019   35258  2201306    62.4 | 32.161 % |
c |     39072 |   66027   144364 |   24220   15463  1056232    68.3 | 32.399 % |
c |     39223 |   66027   144364 |   26642   15614  1063832    68.1 | 32.398 % |
c |     39448 |   65989   144232 |   29307   15824  1069199    67.6 | 32.645 % |
c |     39785 |   65989   144232 |   32238   16161  1097302    67.9 | 32.645 % |
c |     40291 |   65981   144202 |   35461   16621  1122804    67.6 | 32.683 % |
c |     41050 |   65943   144068 |   39008   17366  1152549    66.4 | 32.965 % |
c |     42189 |   65922   143993 |   42908   18497  1213319    65.6 | 33.145 % |
c |     43899 |   65847   143732 |   47199   20160  1342869    66.6 | 33.677 % |
c |     46461 |   65841   143712 |   51919   22700  1414170    62.3 | 33.713 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 37   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47709 |   65842   143719 |   21947   23948  1525631    63.7 | 33.713 % |
c |     47810 |   65842   143719 |   24141   12075   501739    41.6 | 33.738 % |
c |     47960 |   65842   143719 |   26555   12225   505257    41.3 | 33.737 % |
c |     48186 |   65842   143719 |   29211   12451   520665    41.8 | 33.739 % |
c |     48523 |   65842   143719 |   32132   12788   548498    42.9 | 33.737 % |
c |     49029 |   65842   143719 |   35345   13294   569062    42.8 | 33.739 % |
c |     49788 |   65842   143719 |   38880   14053   615685    43.8 | 33.737 % |
c |     50927 |   65827   143668 |   42768   15184   691931    45.6 | 33.810 % |
c |     52635 |   65827   143668 |   47045   16892   815239    48.3 | 33.810 % |
c |     55198 |   65827   143668 |   51749   19455  1149831    59.1 | 33.808 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58660 |   65828   143676 |   21942   22917  1589183    69.3 | 33.808 % |
c |     58763 |   65817   143637 |   24136   11556   966204    83.6 | 33.904 % |
c |     58916 |   65817   143637 |   26549   11709   972705    83.1 | 33.903 % |
c |     59142 |   65817   143637 |   29204   11935   980903    82.2 | 33.903 % |
c |     59479 |   65817   143637 |   32125   12272  1011439    82.4 | 33.903 % |
c |     59985 |   65817   143637 |   35337   12778  1042168    81.6 | 33.905 % |
c |     60745 |   65817   143637 |   38871   13538  1090397    80.5 | 33.905 % |
c |     61887 |   65817   143637 |   42758   14680  1197832    81.6 | 33.903 % |
c |     63595 |   65794   143554 |   47034   16385  1352985    82.6 | 34.116 % |
c |     66157 |   65794   143554 |   51738   18947  1594196    84.1 | 34.116 % |
c |     70003 |   65786   143526 |   56911   22789  2056616    90.2 | 34.187 % |
c |     75770 |   65757   143423 |   62603   28544  2671610    93.6 | 34.438 % |
c |     84419 |   65688   143184 |   68863   37120  3561343    95.9 | 34.936 % |
c |     97393 |   65688   143184 |   75749   50094  5482216   109.4 | 34.934 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113427 |   65689   143189 |   21896   66128  8029016   121.4 | 34.934 % |
c |    113530 |   65689   143189 |   24085   15500  1996071   128.8 | 34.957 % |
c |    113680 |   65666   143106 |   26494   15646  1997845   127.7 | 35.171 % |
c |    113905 |   65666   143106 |   29143   15871  2008454   126.5 | 35.171 % |
c |    114242 |   65666   143106 |   32057   16208  2024166   124.9 | 35.171 % |
c |    114748 |   65666   143106 |   35263   16714  2048805   122.6 | 35.171 % |
c |    115508 |   65657   143077 |   38790   17472  2076044   118.8 | 35.244 % |
c |    116647 |   65657   143077 |   42669   18611  2136811   114.8 | 35.242 % |
c |    118355 |   65657   143077 |   46936   20319  2274732   112.0 | 35.242 % |
c |    120917 |   65657   143077 |   51629   22881  2453330   107.2 | 35.244 % |
c |    124761 |   65657   143077 |   56792   26725  2842571   106.4 | 35.242 % |
c |    130528 |   65657   143077 |   62471   32492  3678443   113.2 | 35.242 % |
c |    139181 |   65657   143077 |   68719   41145  4843533   117.7 | 35.244 % |
c |    152156 |   65657   143077 |   75590   54120  6365063   117.6 | 35.244 % |
c |    171618 |   65657   143077 |   83150   73582  9460080   128.6 | 35.242 % |
c |    200811 |   65648   143046 |   91465   35153  2829959    80.5 | 35.277 % |
c |    244602 |   65639   143015 |  100611   78938  9309858   117.9 | 35.315 % |
c |    310286 |   65639   143015 |  110672   58124  5761368    99.1 | 35.313 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    327737 |   65643   143031 |   21881   75575  7556846   100.0 | 35.313 % |
c |    327839 |   65643   143031 |   24069   14848  1464731    98.6 | 35.323 % |
c |    327990 |   65643   143031 |   26476   14999  1467796    97.9 | 35.323 % |
c |    328215 |   65643   143031 |   29123   15224  1478459    97.1 | 35.323 % |
c |    328552 |   65643   143031 |   32035   15561  1485871    95.5 | 35.323 % |
c |    329058 |   65643   143031 |   35239   16067  1517380    94.4 | 35.323 % |
c |    329817 |   65643   143031 |   38763   16826  1573154    93.5 | 35.326 % |
c |    330957 |   65643   143031 |   42639   17966  1658608    92.3 | 35.323 % |
c |    332665 |   65643   143031 |   46903   19674  1842389    93.6 | 35.323 % |
c |    335227 |   65643   143031 |   51594   22236  2044140    91.9 | 35.323 % |
c |    339075 |   65643   143031 |   56753   26084  2360049    90.5 | 35.326 % |
c |    344841 |   65643   143031 |   62429   31850  2881546    90.5 | 35.323 % |
c |    353491 |   65643   143031 |   68671   40500  3565527    88.0 | 35.326 % |
c |    366465 |   65643   143031 |   75539   53474  4960474    92.8 | 35.323 % |
c |    385928 |   65643   143031 |   83093   72937  6611939    90.7 | 35.323 % |
c |    415120 |   65643   143031 |   91402   34436  3669268   106.6 | 35.323 % |
c |    458911 |   65637   143011 |  100542   78225  9091118   116.2 | 35.361 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 C612 -C611 -C610 -C609 -C608 -C607 -C606 C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 C551 -C550 -C549 -C548 -C547 C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 C360 -C359 -C358 -C357 -C356 -C355 C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 C266 -C265#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 15028
Raw data (stat): 15028 (runsolver) R 15027 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479710014 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 2915 0 0 0 990 8 0 0 25 0 1 0 479710014 13672448 2893 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3338 2893 603 41 0 3297 0
vsize: 13352
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 2915 0 0 0 1989 9 0 0 25 0 1 0 479710014 13672448 2893 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3338 2893 603 41 0 3297 0
vsize: 13352
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 2915 0 0 0 2988 9 0 0 25 0 1 0 479710014 13672448 2893 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3338 2893 603 41 0 3297 0
vsize: 13352
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 3576 0 0 0 3986 11 0 0 25 0 1 0 479710014 16343040 3554 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3990 3554 603 41 0 3949 0
vsize: 15960
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 3894 0 0 0 4985 13 0 0 25 0 1 0 479710014 17817600 3872 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4350 3872 603 41 0 4309 0
vsize: 17400
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 3894 0 0 0 5985 13 0 0 25 0 1 0 479710014 17817600 3872 4294967295 134512640 134672761 3221224560 3221223728 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4350 3872 603 41 0 4309 0
vsize: 17400
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 3894 0 0 0 6985 13 0 0 25 0 1 0 479710014 17817600 3872 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4350 3872 603 41 0 4309 0
vsize: 17400
[startup+80.0021 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 4449 0 0 0 7982 15 0 0 25 0 1 0 479710014 20103168 4427 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4908 4427 603 41 0 4867 0
vsize: 19632
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 5093 0 0 0 8981 17 0 0 25 0 1 0 479710014 22794240 5071 4294967295 134512640 134672761 3221224560 3221223744 134559079 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5565 5071 603 41 0 5524 0
vsize: 22260
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 5758 0 0 0 9979 19 0 0 25 0 1 0 479710014 25477120 5736 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6220 5736 603 41 0 6179 0
vsize: 24880
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 6404 0 0 0 10977 21 0 0 25 0 1 0 479710014 28041216 6382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6846 6382 603 41 0 6805 0
vsize: 27384
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 6983 0 0 0 11976 22 0 0 25 0 1 0 479710014 30449664 6961 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7434 6961 603 41 0 7393 0
vsize: 29736
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 7610 0 0 0 12974 24 0 0 25 0 1 0 479710014 33001472 7588 4294967295 134512640 134672761 3221224560 3221223720 134542657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8057 7588 603 41 0 8016 0
vsize: 32228
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 8284 0 0 0 13972 26 0 0 25 0 1 0 479710014 35692544 8262 4294967295 134512640 134672761 3221224560 3221223664 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8714 8262 603 41 0 8673 0
vsize: 34856
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 8918 0 0 0 14970 28 0 0 25 0 1 0 479710014 38383616 8896 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9371 8896 603 41 0 9330 0
vsize: 37484
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 9421 0 0 0 15969 30 0 0 25 0 1 0 479710014 40398848 9399 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9863 9399 603 41 0 9822 0
vsize: 39452
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 9880 0 0 0 16967 31 0 0 25 0 1 0 479710014 42283008 9858 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10323 9858 603 41 0 10282 0
vsize: 41292
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 17966 32 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 18966 33 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 19966 33 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 20966 33 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 21965 34 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 22965 34 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 23965 34 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 24965 35 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 25964 35 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10052 0 0 0 26964 36 0 0 25 0 1 0 479710014 43212800 10030 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10550 10030 603 41 0 10509 0
vsize: 42200
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10217 0 0 0 27963 37 0 0 25 0 1 0 479710014 43880448 10195 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10713 10195 603 41 0 10672 0
vsize: 42852
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15028
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 10635 0 0 0 28962 38 0 0 25 0 1 0 479710014 45613056 10613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11136 10613 603 41 0 11095 0
vsize: 44544
[startup+300.013 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 15081
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 11080 0 0 0 29960 40 0 0 25 0 1 0 479710014 47349760 11058 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11560 11058 603 41 0 11519 0
vsize: 46240
[startup+310.013 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 15081
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 11508 0 0 0 30959 41 0 0 25 0 1 0 479710014 49090560 11486 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11985 11486 603 41 0 11944 0
vsize: 47940
[startup+320.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 15081
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 11888 0 0 0 31957 43 0 0 25 0 1 0 479710014 50704384 11866 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12379 11866 603 41 0 12338 0
vsize: 49516
[startup+330.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 15081
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12248 0 0 0 32956 44 0 0 25 0 1 0 479710014 52183040 12226 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12740 12226 603 41 0 12699 0
vsize: 50960
[startup+340.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 15081
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12587 0 0 0 33955 45 0 0 25 0 1 0 479710014 53538816 12565 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13071 12565 603 41 0 13030 0
vsize: 52284
[startup+350.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15081
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12951 0 0 0 34954 46 0 0 25 0 1 0 479710014 55013376 12929 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13431 12929 603 41 0 13390 0
vsize: 53724
[startup+360.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15081
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 35955 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+370.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 36955 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+380.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 37955 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+390.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 38955 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+400.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 39955 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+410.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 40956 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223744 134559594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+420.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 41956 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+430.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 42956 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+440.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 43956 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+450.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 44956 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+460.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 45956 46 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+470.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 46956 47 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+480.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 47957 47 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+490.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 48957 47 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+500.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 49956 47 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+510.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12967 0 0 0 50956 47 0 0 25 0 1 0 479710014 55148544 12945 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12945 603 41 0 13423 0
vsize: 53856
[startup+520.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12968 0 0 0 51956 47 0 0 25 0 1 0 479710014 55148544 12946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12946 603 41 0 13423 0
vsize: 53856
[startup+530.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 12971 0 0 0 52956 47 0 0 25 0 1 0 479710014 55148544 12949 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12949 603 41 0 13423 0
vsize: 53856
[startup+540.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 13092 0 0 0 53956 48 0 0 25 0 1 0 479710014 55541760 13070 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13560 13070 603 41 0 13519 0
vsize: 54240
[startup+550.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 13380 0 0 0 54955 49 0 0 25 0 1 0 479710014 56733696 13358 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13851 13358 603 41 0 13810 0
vsize: 55404
[startup+560.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 13651 0 0 0 55953 51 0 0 25 0 1 0 479710014 57802752 13629 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14112 13629 603 41 0 14071 0
vsize: 56448
[startup+570.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 13923 0 0 0 56953 52 0 0 25 0 1 0 479710014 59006976 13901 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13901 603 41 0 14365 0
vsize: 57624
[startup+580.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14235 0 0 0 57952 52 0 0 25 0 1 0 479710014 60211200 14213 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 14213 603 41 0 14659 0
vsize: 58800
[startup+590.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14535 0 0 0 58952 53 0 0 25 0 1 0 479710014 61534208 14513 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15023 14513 603 41 0 14982 0
vsize: 60092
[startup+600.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14619 0 0 0 59952 54 0 0 25 0 1 0 479710014 61796352 14597 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14597 603 41 0 15046 0
vsize: 60348
[startup+610.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14619 0 0 0 60952 54 0 0 25 0 1 0 479710014 61796352 14597 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14597 603 41 0 15046 0
vsize: 60348
[startup+620.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14619 0 0 0 61952 54 0 0 25 0 1 0 479710014 61796352 14597 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14597 603 41 0 15046 0
vsize: 60348
[startup+630.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14619 0 0 0 62952 54 0 0 25 0 1 0 479710014 61796352 14597 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14597 603 41 0 15046 0
vsize: 60348
[startup+640.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15083
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14621 0 0 0 63952 54 0 0 25 0 1 0 479710014 61796352 14599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14599 603 41 0 15046 0
vsize: 60348
[startup+650.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14622 0 0 0 64952 54 0 0 25 0 1 0 479710014 61796352 14600 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14600 603 41 0 15046 0
vsize: 60348
[startup+660.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14622 0 0 0 65952 54 0 0 25 0 1 0 479710014 61796352 14600 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14600 603 41 0 15046 0
vsize: 60348
[startup+670.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14624 0 0 0 66953 54 0 0 25 0 1 0 479710014 61796352 14602 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14602 603 41 0 15046 0
vsize: 60348
[startup+680.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14624 0 0 0 67953 54 0 0 25 0 1 0 479710014 61796352 14602 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14602 603 41 0 15046 0
vsize: 60348
[startup+690.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14624 0 0 0 68953 54 0 0 25 0 1 0 479710014 61796352 14602 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14602 603 41 0 15046 0
vsize: 60348
[startup+700.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 69953 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+710.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 70953 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+720.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 71953 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+730.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 72953 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223664 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+740.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 73953 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134561639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+750.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 74953 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+760.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 75953 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+770.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 76954 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+780.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 77954 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+790.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 78954 54 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+800.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 79954 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+810.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 80954 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+820.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 81954 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223664 134554977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+830.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 82954 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+840.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 83955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+850.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 84955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+860.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 85955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+870.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 86955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223744 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+880.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 87955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+890.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 88955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+900.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 89955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+910.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 90955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+920.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 91955 55 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+930.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 92956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+940.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 93956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+950.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 94956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+960.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 95956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+970.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 96956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+980.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 97956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+990.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 98957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 99957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 100957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 101957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 102957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 103957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 104956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 105957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223664 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 106956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 107956 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 108957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 109957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 110957 56 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14625 0 0 0 111957 57 0 0 25 0 1 0 479710014 61796352 14603 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14603 603 41 0 15046 0
vsize: 60348
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14745 0 0 0 112957 57 0 0 25 0 1 0 479710014 62328832 14723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15217 14723 603 41 0 15176 0
vsize: 60868
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 14999 0 0 0 113957 57 0 0 25 0 1 0 479710014 63393792 14977 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15477 14977 603 41 0 15436 0
vsize: 61908
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 15267 0 0 0 114956 58 0 0 25 0 1 0 479710014 64466944 15245 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15739 15245 603 41 0 15698 0
vsize: 62956
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 15313 0 0 0 115956 58 0 0 25 0 1 0 479710014 64737280 15291 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15805 15291 603 41 0 15764 0
vsize: 63220
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 15313 0 0 0 116956 58 0 0 25 0 1 0 479710014 64737280 15291 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15805 15291 603 41 0 15764 0
vsize: 63220
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 15313 0 0 0 117957 58 0 0 25 0 1 0 479710014 64737280 15291 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15805 15291 603 41 0 15764 0
vsize: 63220
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 15314 0 0 0 118957 58 0 0 25 0 1 0 479710014 64737280 15292 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15805 15292 603 41 0 15764 0
vsize: 63220
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15085
Raw data (stat): 15028 (minisat+) R 15027 11931 11930 0 -1 0 15314 0 0 0 119957 58 0 0 25 0 1 0 479710014 64737280 15292 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15805 15292 603 41 0 15764 0
vsize: 63220
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 15085
Raw data (stat): 15028 (minisat+) Z 15027 11931 11930 0 -1 12 15317 0 0 0 119957 61 0 0 25 0 1 0 479710014 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.08
CPU time (s): 1200.2
CPU user time (s): 1199.58
CPU system time (s): 0.615906
CPU usage (%): 100.009
Max. virtual memory (Kb): 63220
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####