PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-13 21:39:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3056 boxname=wulflinc32 idbench=340 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  45b026c6b351128e9764d865ca917a59  /oldhome/oroussel/tmp/wulflinc32/normalized-frb53-24-2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc32/normalized-frb53-24-2.opb
IDLAUNCH: 3056
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034724 kB
MemFree:        717788 kB
Buffers:         34064 kB
Cached:         170968 kB
SwapCached:       1212 kB
Active:         142548 kB
Inactive:       142812 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        717532 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2244 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25716 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:59:10 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 3056 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94289 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 |   94289   188578 |   31429       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70300     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  169363   364695 |   56454       0        0     nan |  0.000 % |
c |       100 |  168931   363803 |   62099      75      961    12.8 |  0.464 % |
c |       251 |  168226   362304 |   68309     195     2080    10.7 |  1.241 % |
c |       477 |  166908   359478 |   75140     361     4481    12.4 |  2.716 % |
c |       814 |  165085   355491 |   82654     634     6941    10.9 |  4.833 % |
c |      1320 |  161650   347896 |   90919    1002    11746    11.7 |  8.903 % |
c |      2079 |  157439   338515 |  100011    1501    17642    11.8 | 13.952 % |
c |      3218 |  149574   320611 |  110012    2257    27487    12.2 | 23.762 % |
c |      4926 |  140077   298909 |  121014    3343    40938    12.2 | 35.604 % |
c |      7488 |  129263   273622 |  133115    4970    57038    11.5 | 49.390 % |
c |     11332 |  118074   247204 |  146427    7283    85078    11.7 | 64.089 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14173 |  112053   232947 |   37351    8812   110869    12.6 | 64.089 % |
c |     14273 |  111956   232718 |   41086    8872   112201    12.6 | 72.341 % |
c |     14423 |  111733   232187 |   45194    9002   114113    12.7 | 72.561 % |
c |     14649 |  111451   231507 |   49714    9151   118315    12.9 | 72.945 % |
c |     14986 |  111001   230402 |   54685    9390   121727    13.0 | 73.568 % |
c |     15492 |  110268   228664 |   60154    9746   131154    13.5 | 74.539 % |
c |     16252 |  109470   226728 |   66169   10246   139678    13.6 | 75.632 % |
c |     17391 |  108305   223901 |   72786   11038   156782    14.2 | 77.225 % |
c |     19099 |  106843   220411 |   80065   12116   192204    15.9 | 79.176 % |
c |     21662 |  105578   217316 |   88071   13811   254342    18.4 | 80.914 % |
c |     25506 |  104256   214065 |   96878   16859   438700    26.0 | 82.765 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29128 |  104139   213840 |   34713   20366   654650    32.1 | 82.765 % |
c |     29229 |  104025   213562 |   38184   20446   657035    32.1 | 83.099 % |
c |     29380 |  103872   213177 |   42002   20466   657976    32.1 | 83.323 % |
c |     29605 |  103872   213177 |   46203   20691   675471    32.6 | 83.323 % |
c |     29942 |  103872   213177 |   50823   21028   685274    32.6 | 83.323 % |
c |     30448 |  103722   212801 |   55905   21442   702839    32.8 | 83.539 % |
c |     31207 |  103261   211676 |   61496   21792   727090    33.4 | 84.177 % |
c |     32346 |  103261   211676 |   67645   22931   784028    34.2 | 84.177 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33412 |  103252   211633 |   34417   23944   928774    38.8 | 84.177 % |
c |     33512 |  103242   211609 |   37858   24024   929884    38.7 | 84.207 % |
c |     33663 |  103242   211609 |   41644   24175   937156    38.8 | 84.207 % |
c |     33888 |  103242   211609 |   45809   24400   945982    38.8 | 84.207 % |
c |     34225 |  103106   211272 |   50389   24656   961580    39.0 | 84.396 % |
c |     34731 |  103096   211246 |   55428   25109   984488    39.2 | 84.412 % |
c |     35491 |  103053   211129 |   60971   25751  1012426    39.3 | 84.478 % |
c |     36631 |  102901   210759 |   67068   26726  1066796    39.9 | 84.686 % |
c |     38339 |  102881   210709 |   73775   28397  1192012    42.0 | 84.715 % |
c |     40901 |  102881   210709 |   81153   30959  1469684    47.5 | 84.715 % |
c |     44746 |  102871   210685 |   89268   34788  1844984    53.0 | 84.729 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49083 |  102808   210537 |   34269   39065  2552883    65.3 | 84.729 % |
c |     49183 |  102715   210319 |   37695   39094  2554059    65.3 | 84.952 % |
c |     49333 |  102715   210319 |   41465   39244  2564935    65.4 | 84.952 % |
c |     49559 |  102638   210132 |   45612   39228  2570691    65.5 | 85.059 % |
c |     49896 |  102638   210132 |   50173   39565  2591937    65.5 | 85.059 % |
c |     50403 |  102638   210132 |   55190   40072  2655788    66.3 | 85.059 % |
c |     51162 |  102638   210132 |   60709   40831  2713978    66.5 | 85.059 % |
c |     52301 |  102627   210103 |   66780   41795  2803087    67.1 | 85.076 % |
c |     54009 |  102492   209776 |   73458   43288  3004323    69.4 | 85.263 % |
c |     56573 |  102482   209754 |   80804   45807  3307196    72.2 | 85.275 % |
c |     60417 |  102434   209638 |   88884   49598  3816497    76.9 | 85.341 % |
c |     66183 |  102321   209365 |   97773   54712  4533488    82.9 | 85.496 % |
c |     74832 |  102098   208818 |  107550   62430  5539945    88.7 | 85.806 % |
c |     87807 |  101884   208284 |  118305   75224  8117231   107.9 | 86.117 % |
c ==============================================================================
c [1mFound solution: -46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89873 |  101873   208219 |   33957   77213  8366826   108.4 | 86.117 % |
c |     89973 |  101813   208079 |   37352   77250  8370963   108.4 | 86.209 % |
c |     90123 |  101813   208079 |   41087   77400  8384920   108.3 | 86.209 % |
c |     90348 |  101813   208079 |   45196   77625  8402830   108.2 | 86.209 % |
c |     90685 |  101813   208079 |   49716   77962  8425118   108.1 | 86.209 % |
c |     91191 |  101808   208066 |   54688   78418  8477500   108.1 | 86.217 % |
c |     91950 |  101769   207969 |   60156   79147  8535292   107.8 | 86.273 % |
c |     93089 |  101732   207878 |   66172   79954  8650341   108.2 | 86.324 % |
c |     94797 |  101691   207781 |   72789   81587  8836109   108.3 | 86.378 % |
c |     97360 |  101678   207750 |   80068   84139  9093070   108.1 | 86.396 % |
c |    101204 |  101587   207532 |   88075   87350  9467343   108.4 | 86.516 % |
c |    106970 |  101584   207525 |   96883   93115 10262644   110.2 | 86.520 % |
c |    115619 |  101584   207525 |  106571  101764 11400274   112.0 | 86.520 % |
c ==============================================================================
c [1mFound solution: -47[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128246 |  101576   207519 |   33858  113993 13276183   116.5 | 86.520 % |
c |    128346 |  101576   207519 |   37243   20346  1966312    96.6 | 86.569 % |
c |    128496 |  101576   207519 |   40968   20496  1972565    96.2 | 86.569 % |
c |    128722 |  101576   207519 |   45064   20722  1990233    96.0 | 86.569 % |
c |    129059 |  101576   207519 |   49571   21059  2010034    95.4 | 86.569 % |
c |    129565 |  101573   207512 |   54528   21564  2043549    94.8 | 86.573 % |
c |    130325 |  101573   207512 |   59981   22324  2119304    94.9 | 86.573 % |
c |    131466 |  101573   207512 |   65979   23465  2227953    94.9 | 86.573 % |
c |    133174 |  101566   207497 |   72577   25171  2440505    97.0 | 86.580 % |
c |    135736 |  101564   207493 |   79835   27732  2748292    99.1 | 86.582 % |
c |    139581 |  101564   207493 |   87818   31577  3280586   103.9 | 86.582 % |
c |    145347 |  101564   207493 |   96600   37343  4140110   110.9 | 86.582 % |
c |    153996 |  101564   207493 |  106260   45992  5223572   113.6 | 86.582 % |
c |    166970 |  101517   207383 |  116886   58757  6847744   116.5 | 86.641 % |
c |    186431 |  101502   207348 |  128575   78195  9333628   119.4 | 86.660 % |
c |    215624 |  101465   207263 |  141433  107203 13487587   125.8 | 86.705 % |
c |    259413 |  101459   207249 |  155576  150988 19357146   128.2 | 86.712 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -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 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/53 12087
Raw data (stat): 12087 (runsolver) R 12086 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479251698 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.88 0.94 0.90 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5661 0 0 0 984 14 0 0 25 0 1 0 479251698 26193920 5639 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6395 5639 603 41 0 6354 0
vsize: 25580
[startup+20.0021 s]
Raw data (loadavg): 0.89 0.94 0.90 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5671 0 0 0 1984 14 0 0 25 0 1 0 479251698 26193920 5649 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6395 5649 603 41 0 6354 0
vsize: 25580
[startup+30.0028 s]
Raw data (loadavg): 0.91 0.94 0.90 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5677 0 0 0 2984 14 0 0 25 0 1 0 479251698 26329088 5655 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6428 5655 603 41 0 6387 0
vsize: 25712
[startup+40.0038 s]
Raw data (loadavg): 0.92 0.94 0.90 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5683 0 0 0 3984 15 0 0 25 0 1 0 479251698 26329088 5661 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6428 5661 603 41 0 6387 0
vsize: 25712
[startup+50.0054 s]
Raw data (loadavg): 0.93 0.95 0.90 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5691 0 0 0 4984 15 0 0 25 0 1 0 479251698 26329088 5669 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6428 5669 603 41 0 6387 0
vsize: 25712
[startup+60.0064 s]
Raw data (loadavg): 0.94 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5699 0 0 0 5984 15 0 0 25 0 1 0 479251698 26329088 5677 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6428 5677 603 41 0 6387 0
vsize: 25712
[startup+70.0079 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5700 0 0 0 6984 15 0 0 25 0 1 0 479251698 26329088 5678 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6428 5678 603 41 0 6387 0
vsize: 25712
[startup+80.0086 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5708 0 0 0 7984 15 0 0 25 0 1 0 479251698 26460160 5686 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6460 5686 603 41 0 6419 0
vsize: 25840
[startup+90.0094 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5721 0 0 0 8984 15 0 0 25 0 1 0 479251698 26460160 5699 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6460 5699 603 41 0 6419 0
vsize: 25840
[startup+100.01 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5856 0 0 0 9984 16 0 0 25 0 1 0 479251698 27226112 5834 4294967295 134512640 134672761 3221224624 3221223344 134545043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6647 5834 603 41 0 6606 0
vsize: 26588
[startup+110.011 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 5930 0 0 0 10984 16 0 0 25 0 1 0 479251698 27779072 5908 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6782 5908 603 41 0 6741 0
vsize: 27128
[startup+120.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 6126 0 0 0 11983 17 0 0 25 0 1 0 479251698 28454912 6104 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6947 6104 603 41 0 6906 0
vsize: 27788
[startup+130.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 6487 0 0 0 12982 18 0 0 25 0 1 0 479251698 30031872 6456 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7332 6456 603 41 0 7291 0
vsize: 29328
[startup+140.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 6872 0 0 0 13980 20 0 0 25 0 1 0 479251698 31571968 6832 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 6832 603 41 0 7667 0
vsize: 30832
[startup+150.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 7384 0 0 0 14979 21 0 0 25 0 1 0 479251698 33595392 7344 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8202 7344 603 41 0 8161 0
vsize: 32808
[startup+160.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 7934 0 0 0 15978 23 0 0 25 0 1 0 479251698 36003840 7894 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8790 7894 603 41 0 8749 0
vsize: 35160
[startup+170.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 8595 0 0 0 16975 25 0 0 25 0 1 0 479251698 38617088 8546 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9428 8546 603 41 0 9387 0
vsize: 37712
[startup+180.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 9033 0 0 0 17973 28 0 0 25 0 1 0 479251698 40366080 8984 4294967295 134512640 134672761 3221224624 3221223792 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9855 8984 603 41 0 9814 0
vsize: 39420
[startup+190.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 9564 0 0 0 18972 29 0 0 25 0 1 0 479251698 42504192 9515 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10377 9515 603 41 0 10336 0
vsize: 41508
[startup+200.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 10002 0 0 0 19971 31 0 0 25 0 1 0 479251698 44384256 9953 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10836 9953 603 41 0 10795 0
vsize: 43344
[startup+210.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 10485 0 0 0 20970 32 0 0 25 0 1 0 479251698 46256128 10436 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11293 10437 603 41 0 11252 0
vsize: 45172
[startup+220.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 10962 0 0 0 21968 33 0 0 25 0 1 0 479251698 48275456 10913 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11786 10913 603 41 0 11745 0
vsize: 47144
[startup+230.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 11376 0 0 0 22968 34 0 0 25 0 1 0 479251698 49881088 11327 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12178 11327 603 41 0 12137 0
vsize: 48712
[startup+240.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 11729 0 0 0 23967 35 0 0 25 0 1 0 479251698 51355648 11680 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12538 11680 603 41 0 12497 0
vsize: 50152
[startup+250.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 12103 0 0 0 24966 36 0 0 25 0 1 0 479251698 52834304 12054 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12899 12054 603 41 0 12858 0
vsize: 51596
[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 12654 0 0 0 25965 37 0 0 25 0 1 0 479251698 55386112 12605 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13522 12605 603 41 0 13481 0
vsize: 54088
[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 13146 0 0 0 26964 39 0 0 25 0 1 0 479251698 57384960 13097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14010 13097 603 41 0 13969 0
vsize: 56040
[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 13652 0 0 0 27962 41 0 0 25 0 1 0 479251698 59387904 13603 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14499 13603 603 41 0 14458 0
vsize: 57996
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 14146 0 0 0 28961 42 0 0 25 0 1 0 479251698 61513728 14097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15018 14097 603 41 0 14977 0
vsize: 60072
[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 14563 0 0 0 29959 44 0 0 25 0 1 0 479251698 63115264 14514 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15409 14514 603 41 0 15368 0
vsize: 61636
[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 14818 0 0 0 30958 44 0 0 25 0 1 0 479251698 64110592 14761 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15652 14761 603 41 0 15611 0
vsize: 62608
[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 15067 0 0 0 31957 45 0 0 25 0 1 0 479251698 65187840 15010 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15915 15010 603 41 0 15874 0
vsize: 63660
[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 15418 0 0 0 32956 47 0 0 25 0 1 0 479251698 66666496 15361 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16276 15361 603 41 0 16235 0
vsize: 65104
[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 15648 0 0 0 33956 47 0 0 25 0 1 0 479251698 67477504 15591 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16474 15591 603 41 0 16433 0
vsize: 65896
[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 15915 0 0 0 34955 48 0 0 25 0 1 0 479251698 68558848 15858 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16738 15858 603 41 0 16697 0
vsize: 66952
[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 16267 0 0 0 35954 50 0 0 25 0 1 0 479251698 70017024 16210 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17094 16210 603 41 0 17053 0
vsize: 68376
[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 16575 0 0 0 36953 51 0 0 25 0 1 0 479251698 71356416 16518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17421 16518 603 41 0 17380 0
vsize: 69684
[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 16896 0 0 0 37951 52 0 0 25 0 1 0 479251698 72556544 16839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17714 16839 603 41 0 17673 0
vsize: 70856
[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 17161 0 0 0 38951 53 0 0 25 0 1 0 479251698 73748480 17104 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18005 17104 603 41 0 17964 0
vsize: 72020
[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 17466 0 0 0 39950 54 0 0 25 0 1 0 479251698 74952704 17409 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18299 17409 603 41 0 18258 0
vsize: 73196
[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 17750 0 0 0 40949 56 0 0 25 0 1 0 479251698 76152832 17693 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 17693 603 41 0 18551 0
vsize: 74368
[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 18029 0 0 0 41948 56 0 0 25 0 1 0 479251698 77225984 17972 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18854 17972 603 41 0 18813 0
vsize: 75416
[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 18295 0 0 0 42948 57 0 0 25 0 1 0 479251698 78290944 18238 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19114 18238 603 41 0 19073 0
vsize: 76456
[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 18579 0 0 0 43947 58 0 0 25 0 1 0 479251698 79503360 18522 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18522 603 41 0 19369 0
vsize: 77640
[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 18918 0 0 0 44946 59 0 0 25 0 1 0 479251698 80834560 18861 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19735 18861 603 41 0 19694 0
vsize: 78940
[startup+460.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19280 0 0 0 45945 60 0 0 25 0 1 0 479251698 82313216 19223 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20096 19223 603 41 0 20055 0
vsize: 80384
[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19640 0 0 0 46944 62 0 0 25 0 1 0 479251698 83767296 19583 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20451 19583 603 41 0 20410 0
vsize: 81804
[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 47943 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223924 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 48943 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 49943 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 50943 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+520.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 51944 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 52944 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 53944 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 54944 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 55944 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 56944 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+580.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 57944 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+590.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 58945 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 59945 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+610.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 60945 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 61945 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 62946 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+640.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 63946 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+650.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 64946 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 65946 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+670.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 66946 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 67946 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 68946 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 69947 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 70947 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+720.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 71947 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 72947 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 73948 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223728 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 74948 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223728 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 75948 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+770.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 19956 0 0 0 76948 63 0 0 25 0 1 0 479251698 84971520 19890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20745 19890 603 41 0 20704 0
vsize: 82980
[startup+780.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 20288 0 0 0 77947 64 0 0 25 0 1 0 479251698 86441984 20222 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21104 20222 603 41 0 21063 0
vsize: 84416
[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 20590 0 0 0 78946 66 0 0 25 0 1 0 479251698 87642112 20524 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21397 20524 603 41 0 21356 0
vsize: 85588
[startup+800.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 20858 0 0 0 79946 66 0 0 25 0 1 0 479251698 88711168 20792 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21658 20792 603 41 0 21617 0
vsize: 86632
[startup+810.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 21092 0 0 0 80945 67 0 0 25 0 1 0 479251698 89640960 21026 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21885 21026 603 41 0 21844 0
vsize: 87540
[startup+820.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 21344 0 0 0 81944 68 0 0 25 0 1 0 479251698 90705920 21278 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22145 21278 603 41 0 22104 0
vsize: 88580
[startup+830.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 21642 0 0 0 82943 69 0 0 25 0 1 0 479251698 91914240 21576 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22440 21576 603 41 0 22399 0
vsize: 89760
[startup+840.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 21917 0 0 0 83943 70 0 0 25 0 1 0 479251698 93118464 21851 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22734 21851 603 41 0 22693 0
vsize: 90936
[startup+850.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 22211 0 0 0 84942 71 0 0 25 0 1 0 479251698 94318592 22145 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23027 22145 603 41 0 22986 0
vsize: 92108
[startup+860.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 22470 0 0 0 85941 72 0 0 25 0 1 0 479251698 95252480 22404 4294967295 134512640 134672761 3221224624 3221223760 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23255 22404 603 41 0 23214 0
vsize: 93020
[startup+870.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 22715 0 0 0 86940 73 0 0 25 0 1 0 479251698 96317440 22649 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23515 22649 603 41 0 23474 0
vsize: 94060
[startup+880.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 22974 0 0 0 87940 74 0 0 25 0 1 0 479251698 97386496 22908 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23776 22908 603 41 0 23735 0
vsize: 95104
[startup+890.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 23262 0 0 0 88938 76 0 0 25 0 1 0 479251698 98590720 23196 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24070 23196 603 41 0 24029 0
vsize: 96280
[startup+900.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 23523 0 0 0 89938 77 0 0 25 0 1 0 479251698 100184064 23457 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24459 23457 603 41 0 24418 0
vsize: 97836
[startup+910.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 23789 0 0 0 90937 77 0 0 25 0 1 0 479251698 101249024 23723 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24719 23723 603 41 0 24678 0
vsize: 98876
[startup+920.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 24050 0 0 0 91937 78 0 0 25 0 1 0 479251698 102313984 23984 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24979 23984 603 41 0 24938 0
vsize: 99916
[startup+930.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 24302 0 0 0 92936 79 0 0 25 0 1 0 479251698 103256064 24236 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25209 24236 603 41 0 25168 0
vsize: 100836
[startup+940.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 24542 0 0 0 93936 79 0 0 25 0 1 0 479251698 104329216 24476 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24476 603 41 0 25430 0
vsize: 101884
[startup+950.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 24794 0 0 0 94935 80 0 0 25 0 1 0 479251698 105259008 24728 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25698 24728 603 41 0 25657 0
vsize: 102792
[startup+960.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 25023 0 0 0 95935 81 0 0 25 0 1 0 479251698 106196992 24957 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25927 24957 603 41 0 25886 0
vsize: 103708
[startup+970.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 25256 0 0 0 96934 82 0 0 25 0 1 0 479251698 107126784 25190 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26154 25190 603 41 0 26113 0
vsize: 104616
[startup+980.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 25490 0 0 0 97933 84 0 0 25 0 1 0 479251698 108191744 25424 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26414 25424 603 41 0 26373 0
vsize: 105656
[startup+990.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 25717 0 0 0 98932 85 0 0 25 0 1 0 479251698 109121536 25651 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26641 25651 603 41 0 26600 0
vsize: 106564
[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 25945 0 0 0 99931 86 0 0 25 0 1 0 479251698 110055424 25879 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26869 25879 603 41 0 26828 0
vsize: 107476
[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 26163 0 0 0 100930 87 0 0 25 0 1 0 479251698 110850048 26097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27063 26097 603 41 0 27022 0
vsize: 108252
[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 26372 0 0 0 101930 88 0 0 25 0 1 0 479251698 111775744 26306 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27289 26306 603 41 0 27248 0
vsize: 109156
[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 26616 0 0 0 102929 89 0 0 25 0 1 0 479251698 112705536 26550 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27516 26550 603 41 0 27475 0
vsize: 110064
[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 26847 0 0 0 103928 89 0 0 25 0 1 0 479251698 113643520 26781 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27745 26781 603 41 0 27704 0
vsize: 110980
[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 27073 0 0 0 104928 90 0 0 25 0 1 0 479251698 114573312 27007 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27972 27007 603 41 0 27931 0
vsize: 111888
[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 27308 0 0 0 105928 90 0 0 25 0 1 0 479251698 115621888 27242 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28228 27242 603 41 0 28187 0
vsize: 112912
[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 27551 0 0 0 106927 91 0 0 25 0 1 0 479251698 116559872 27485 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28457 27485 603 41 0 28416 0
vsize: 113828
[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 27773 0 0 0 107927 92 0 0 25 0 1 0 479251698 117518336 27707 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28691 27707 603 41 0 28650 0
vsize: 114764
[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 28014 0 0 0 108926 93 0 0 25 0 1 0 479251698 118456320 27948 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28920 27948 603 41 0 28879 0
vsize: 115680
[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 28244 0 0 0 109926 94 0 0 25 0 1 0 479251698 119386112 28178 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29147 28178 603 41 0 29106 0
vsize: 116588
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 28471 0 0 0 110925 94 0 0 25 0 1 0 479251698 120315904 28405 4294967295 134512640 134672761 3221224624 3221223808 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29374 28405 603 41 0 29333 0
vsize: 117496
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 28707 0 0 0 111925 95 0 0 25 0 1 0 479251698 121237504 28641 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29599 28641 603 41 0 29558 0
vsize: 118396
[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 28938 0 0 0 112924 96 0 0 25 0 1 0 479251698 122175488 28872 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29828 28872 603 41 0 29787 0
vsize: 119312
[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 29160 0 0 0 113924 96 0 0 25 0 1 0 479251698 123109376 29094 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30056 29094 603 41 0 30015 0
vsize: 120224
[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 29358 0 0 0 114923 98 0 0 25 0 1 0 479251698 123908096 29292 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30251 29292 603 41 0 30210 0
vsize: 121004
[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 29546 0 0 0 115923 98 0 0 25 0 1 0 479251698 124706816 29480 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30446 29480 603 41 0 30405 0
vsize: 121784
[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 29695 0 0 0 116923 98 0 0 25 0 1 0 479251698 125239296 29629 4294967295 134512640 134672761 3221224624 3221223728 134559771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30576 29629 603 41 0 30535 0
vsize: 122304
[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 29871 0 0 0 117922 99 0 0 25 0 1 0 479251698 126042112 29805 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30772 29805 603 41 0 30731 0
vsize: 123088
[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 30051 0 0 0 118921 100 0 0 25 0 1 0 479251698 126709760 29985 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30935 29985 603 41 0 30894 0
vsize: 123740
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12087
Raw data (stat): 12087 (minisat+) R 12086 7987 7986 0 -1 0 30224 0 0 0 119921 100 0 0 25 0 1 0 479251698 127512576 30158 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31131 30158 603 41 0 31090 0
vsize: 124524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 12087
Raw data (stat): 12087 (minisat+) Z 12086 7987 7986 0 -1 12 30227 0 0 0 119921 106 0 0 24 0 1 0 479251698 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.17
CPU time (s): 1200.29
CPU user time (s): 1199.22
CPU system time (s): 1.06884
CPU usage (%): 100.009
Max. virtual memory (Kb): 124524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####