PB'05 competition: run trace

Some explanations

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

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        874172 kB
Buffers:         28220 kB
Cached:         111996 kB
SwapCached:          0 kB
Active:          38680 kB
Inactive:       104440 kB
HighTotal:      131008 kB
HighFree:        15400 kB
LowTotal:       903652 kB
LowFree:        858772 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11772 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:13:59 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4471 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80851 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 |   80851   161702 |   26950       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  148737   320958 |   49579       0        0     nan |  0.000 % |
c |       101 |  148366   320193 |   54536      85      765     9.0 |  0.441 % |
c |       252 |  148029   319484 |   59990     220     3072    14.0 |  0.844 % |
c |       477 |  147140   317584 |   65989     414     5422    13.1 |  1.937 % |
c |       814 |  145503   314007 |   72588     695    10180    14.6 |  4.025 % |
c |      1320 |  141871   306005 |   79847    1052    14339    13.6 |  8.753 % |
c |      2079 |  136023   292923 |   87832    1565    21384    13.7 | 16.582 % |
c |      3218 |  130632   280671 |   96615    2487    32283    13.0 | 23.974 % |
c |      4926 |  123081   263362 |  106276    3797    51144    13.5 | 34.454 % |
c |      7488 |  115042   244888 |  116904    5568    76837    13.8 | 45.531 % |
c |     11332 |  106902   225592 |  128595    8647   126243    14.6 | 57.367 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12189 |  105355   221989 |   35118    9206   138743    15.1 | 57.367 % |
c |     12292 |  105334   221942 |   38629    9300   142332    15.3 | 59.672 % |
c |     12442 |  105154   221511 |   42492    9437   144616    15.3 | 59.940 % |
c |     12668 |  104547   220088 |   46742    9550   146897    15.4 | 60.812 % |
c |     13005 |  104266   219414 |   51416    9700   149137    15.4 | 61.231 % |
c |     13511 |  102353   214845 |   56557    9851   154585    15.7 | 64.142 % |
c |     14271 |  101471   212704 |   62213   10471   168910    16.1 | 65.388 % |
c |     15410 |  100525   210483 |   68435   11341   190635    16.8 | 66.819 % |
c |     17118 |   98376   205358 |   75278   12589   222288    17.7 | 69.882 % |
c |     19680 |   97425   203063 |   82806   14811   278397    18.8 | 71.285 % |
c ==============================================================================
c [1mFound solution: -38[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 |     19987 |   96638   201152 |   32212   14981   283316    18.9 | 71.285 % |
c |     20087 |   96638   201152 |   35433   15081   285189    18.9 | 72.422 % |
c |     20237 |   96439   200654 |   38976   15146   288150    19.0 | 72.733 % |
c |     20462 |   96306   200334 |   42874   15335   293321    19.1 | 72.932 % |
c |     20799 |   95886   199340 |   47161   15583   300834    19.3 | 73.553 % |
c |     21306 |   95774   199086 |   51877   16064   315316    19.6 | 73.706 % |
c |     22066 |   95551   198555 |   57065   16757   339492    20.3 | 74.033 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22573 |   95160   197669 |   31720   17015   350326    20.6 | 74.033 % |
c |     22673 |   95160   197669 |   34892   17115   356501    20.8 | 74.686 % |
c |     22823 |   95106   197535 |   38381   17261   360565    20.9 | 74.772 % |
c |     23049 |   95013   197310 |   42219   17466   365076    20.9 | 74.910 % |
c |     23386 |   94966   197201 |   46441   17776   378604    21.3 | 74.975 % |
c |     23892 |   94961   197190 |   51085   18276   390433    21.4 | 74.981 % |
c |     24652 |   94399   195810 |   56193   18675   406360    21.8 | 75.842 % |
c |     25792 |   94283   195526 |   61813   19618   439777    22.4 | 76.021 % |
c |     27501 |   93887   194570 |   67994   21188   551252    26.0 | 76.623 % |
c |     30063 |   93580   193835 |   74794   23586   661515    28.0 | 77.085 % |
c |     33907 |   92526   191288 |   82273   26622   855765    32.1 | 78.683 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34660 |   92501   191256 |   30833   27346   890259    32.6 | 78.683 % |
c |     34760 |   92374   190951 |   33916   27407   892203    32.6 | 78.925 % |
c |     34910 |   92374   190951 |   37307   27557   897352    32.6 | 78.925 % |
c |     35135 |   92325   190828 |   41038   27771   909011    32.7 | 78.996 % |
c |     35472 |   92325   190828 |   45142   28108   929804    33.1 | 78.996 % |
c |     35978 |   92325   190828 |   49656   28614   952436    33.3 | 78.996 % |
c |     36737 |   91933   189887 |   54622   29190   998234    34.2 | 79.580 % |
c |     37877 |   91668   189231 |   60084   30184  1050966    34.8 | 79.977 % |
c |     39585 |   91179   188051 |   66093   31104  1123554    36.1 | 80.703 % |
c |     42147 |   90991   187592 |   72702   33536  1352386    40.3 | 80.990 % |
c |     45991 |   90915   187410 |   79972   37245  1889303    50.7 | 81.102 % |
c |     51757 |   90762   187040 |   87970   42879  2343683    54.7 | 81.333 % |
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 |     52914 |   90753   186986 |   30251   43937  2470581    56.2 | 81.333 % |
c |     53014 |   90753   186986 |   33276   44037  2472887    56.2 | 81.351 % |
c |     53164 |   90753   186986 |   36603   44187  2487369    56.3 | 81.351 % |
c |     53390 |   90753   186986 |   40264   44413  2502524    56.3 | 81.351 % |
c |     53727 |   90753   186986 |   44290   44750  2517712    56.3 | 81.351 % |
c |     54234 |   90712   186891 |   48719   45092  2552226    56.6 | 81.407 % |
c |     54995 |   90712   186891 |   53591   45853  2626768    57.3 | 81.407 % |
c |     56134 |   90698   186857 |   58950   46911  2726470    58.1 | 81.429 % |
c |     57843 |   90611   186643 |   64845   48530  2837380    58.5 | 81.556 % |
c |     60405 |   90521   186429 |   71330   50928  3048163    59.9 | 81.685 % |
c |     64249 |   90508   186398 |   78463   54678  3459802    63.3 | 81.705 % |
c |     70016 |   90366   186066 |   86309   60273  4054487    67.3 | 81.907 % |
c |     78665 |   90114   185438 |   94940   68614  5012115    73.0 | 82.308 % |
c |     91640 |   89808   184690 |  104434   80924  6476449    80.0 | 82.780 % |
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 |    101349 |   89784   184660 |   29928   90515  7625234    84.2 | 82.780 % |
c |    101449 |   89740   184546 |   32920   23637  1615649    68.4 | 82.927 % |
c |    101600 |   89736   184536 |   36212   23784  1622993    68.2 | 82.933 % |
c |    101825 |   89736   184536 |   39834   24009  1640600    68.3 | 82.933 % |
c |    102162 |   89658   184344 |   43817   24307  1661876    68.4 | 83.056 % |
c |    102668 |   89497   183949 |   48199   24754  1694957    68.5 | 83.305 % |
c |    103427 |   89497   183949 |   53019   25513  1767199    69.3 | 83.305 % |
c |    104566 |   89497   183949 |   58321   26652  1884370    70.7 | 83.305 % |
c |    106275 |   89373   183652 |   64153   28323  2061056    72.8 | 83.490 % |
c |    108837 |   89373   183652 |   70568   30885  2343424    75.9 | 83.490 % |
c |    112681 |   89339   183568 |   77625   34664  2898101    83.6 | 83.544 % |
c |    118447 |   88995   182758 |   85388   40297  3742322    92.9 | 84.037 % |
c |    127096 |   88992   182751 |   93926   48945  4973106   101.6 | 84.041 % |
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 |    128864 |   88967   182666 |   29655   50677  5251581   103.6 | 84.041 % |
c |    128964 |   88962   182655 |   32620   50775  5256860   103.5 | 84.087 % |
c |    129114 |   88962   182655 |   35882   50925  5267190   103.4 | 84.087 % |
c |    129339 |   88962   182655 |   39470   51150  5283543   103.3 | 84.087 % |
c |    129677 |   88962   182655 |   43417   51488  5324792   103.4 | 84.087 % |
c |    130183 |   88962   182655 |   47759   51994  5375997   103.4 | 84.087 % |
c |    130942 |   88962   182655 |   52535   52753  5461119   103.5 | 84.087 % |
c |    132081 |   88962   182655 |   57789   53892  5567309   103.3 | 84.087 % |
c |    133790 |   88962   182655 |   63568   55601  5753628   103.5 | 84.087 % |
c |    136353 |   88870   182433 |   69924   58139  6016906   103.5 | 84.220 % |
c |    140197 |   88770   182167 |   76917   61962  6470826   104.4 | 84.399 % |
c |    145963 |   88768   182163 |   84609   67727  7108180   105.0 | 84.401 % |
c |    154612 |   88725   182047 |   93070   76332  8360934   109.5 | 84.474 % |
c |    167586 |   88673   181922 |  102377   89282 10392161   116.4 | 84.554 % |
c |    187048 |   88609   181774 |  112614  108730 13218100   121.6 | 84.644 % |
c |    216240 |   88592   181733 |  123876  137917 17842959   129.4 | 84.670 % |
c |    260030 |   88397   181266 |  136263   36498  4124381   113.0 | 84.963 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 C625 -C624 -C623 -C622 C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -#### 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.91 0.95 0.90 2/55 3724
Raw data (stat): 3724 (runsolver) R 3723 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 358408678 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 4927 0 0 0 986 13 0 0 25 0 1 0 358408678 23285760 4905 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5685 4905 603 41 0 5644 0
vsize: 22740
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 4936 0 0 0 1985 13 0 0 25 0 1 0 358408678 23285760 4914 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5685 4914 603 41 0 5644 0
vsize: 22740
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 4946 0 0 0 2986 13 0 0 25 0 1 0 358408678 23285760 4924 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5685 4924 603 41 0 5644 0
vsize: 22740
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 4958 0 0 0 3985 14 0 0 25 0 1 0 358408678 23420928 4936 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5718 4936 603 41 0 5677 0
vsize: 22872
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 4968 0 0 0 4985 14 0 0 25 0 1 0 358408678 23420928 4946 4294967295 134512640 134672761 3221224560 3221223776 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5718 4946 603 41 0 5677 0
vsize: 22872
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 4990 0 0 0 5985 14 0 0 25 0 1 0 358408678 23552000 4968 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5750 4968 603 41 0 5709 0
vsize: 23000
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 5032 0 0 0 6985 14 0 0 25 0 1 0 358408678 23719936 5010 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5791 5010 603 41 0 5750 0
vsize: 23164
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 5162 0 0 0 7984 15 0 0 25 0 1 0 358408678 24514560 5140 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5985 5140 603 41 0 5944 0
vsize: 23940
[startup+90.0032 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 5265 0 0 0 8984 15 0 0 25 0 1 0 358408678 24920064 5243 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6084 5243 603 41 0 6043 0
vsize: 24336
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 5423 0 0 0 9983 16 0 0 25 0 1 0 358408678 25645056 5401 4294967295 134512640 134672761 3221224560 3221223776 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6261 5401 603 41 0 6220 0
vsize: 25044
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 5806 0 0 0 10982 17 0 0 25 0 1 0 358408678 27262976 5784 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6656 5784 603 41 0 6615 0
vsize: 26624
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 6078 0 0 0 11982 18 0 0 25 0 1 0 358408678 28311552 6056 4294967295 134512640 134672761 3221224560 3221223664 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6912 6056 603 41 0 6871 0
vsize: 27648
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 6461 0 0 0 12981 19 0 0 25 0 1 0 358408678 30056448 6439 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7338 6439 603 41 0 7297 0
vsize: 29352
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 7073 0 0 0 13980 20 0 0 25 0 1 0 358408678 32473088 7051 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7928 7051 603 41 0 7887 0
vsize: 31712
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 7546 0 0 0 14979 21 0 0 25 0 1 0 358408678 34357248 7524 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8388 7524 603 41 0 8347 0
vsize: 33552
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 7969 0 0 0 15978 22 0 0 25 0 1 0 358408678 36167680 7947 4294967295 134512640 134672761 3221224560 3221223776 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8830 7947 603 41 0 8789 0
vsize: 35320
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 8324 0 0 0 16977 24 0 0 25 0 1 0 358408678 37511168 8302 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9158 8302 603 41 0 9117 0
vsize: 36632
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 8795 0 0 0 17976 25 0 0 25 0 1 0 358408678 39510016 8773 4294967295 134512640 134672761 3221224560 3221223664 134560150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9646 8773 603 41 0 9605 0
vsize: 38584
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 9177 0 0 0 18975 26 0 0 25 0 1 0 358408678 40996864 9155 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10009 9155 603 41 0 9968 0
vsize: 40036
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 9623 0 0 0 19974 27 0 0 25 0 1 0 358408678 42876928 9601 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10468 9601 603 41 0 10427 0
vsize: 41872
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 9973 0 0 0 20973 28 0 0 25 0 1 0 358408678 44216320 9951 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10795 9951 603 41 0 10754 0
vsize: 43180
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 10395 0 0 0 21971 30 0 0 25 0 1 0 358408678 46223360 10373 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11285 10373 603 41 0 11244 0
vsize: 45140
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 10827 0 0 0 22970 31 0 0 25 0 1 0 358408678 47964160 10805 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11710 10805 603 41 0 11669 0
vsize: 46840
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 11175 0 0 0 23969 33 0 0 25 0 1 0 358408678 49434624 11153 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12069 11153 603 41 0 12028 0
vsize: 48276
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 11549 0 0 0 24967 34 0 0 25 0 1 0 358408678 50909184 11527 4294967295 134512640 134672761 3221224560 3221223744 134559179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12429 11527 603 41 0 12388 0
vsize: 49716
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 11903 0 0 0 25967 35 0 0 25 0 1 0 358408678 52383744 11881 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12789 11881 603 41 0 12748 0
vsize: 51156
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 12175 0 0 0 26966 36 0 0 25 0 1 0 358408678 53456896 12153 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13051 12153 603 41 0 13010 0
vsize: 52204
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 12474 0 0 0 27965 37 0 0 25 0 1 0 358408678 54657024 12452 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13344 12452 603 41 0 13303 0
vsize: 53376
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 12861 0 0 0 28965 38 0 0 25 0 1 0 358408678 56250368 12839 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13733 12839 603 41 0 13692 0
vsize: 54932
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13277 0 0 0 29964 39 0 0 25 0 1 0 358408678 57995264 13255 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14159 13255 603 41 0 14118 0
vsize: 56636
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 30963 40 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 31963 40 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 32963 40 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 33963 40 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 34963 40 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3724
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 35963 40 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+370.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 3777
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 36962 41 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+380.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 3777
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 37962 41 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+390.019 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 3777
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 38962 41 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+400.019 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 3777
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 39962 41 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+410.019 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 3777
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 40962 41 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+420.019 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 3777
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 41963 41 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+430.019 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 3779
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 42963 41 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+440.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 3779
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13323 0 0 0 43963 41 0 0 25 0 1 0 358408678 58126336 13301 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13301 603 41 0 14150 0
vsize: 56764
[startup+450.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 13670 0 0 0 44962 42 0 0 25 0 1 0 358408678 59600896 13648 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14551 13648 603 41 0 14510 0
vsize: 58204
[startup+460.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 14011 0 0 0 45962 43 0 0 25 0 1 0 358408678 60948480 13989 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14880 13989 603 41 0 14839 0
vsize: 59520
[startup+470.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 14366 0 0 0 46961 44 0 0 25 0 1 0 358408678 62418944 14344 4294967295 134512640 134672761 3221224560 3221223744 134558923 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15239 14344 603 41 0 15198 0
vsize: 60956
[startup+480.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 14635 0 0 0 47961 44 0 0 25 0 1 0 358408678 63496192 14613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15502 14613 603 41 0 15461 0
vsize: 62008
[startup+490.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 15029 0 0 0 48960 46 0 0 25 0 1 0 358408678 65101824 15007 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15894 15007 603 41 0 15853 0
vsize: 63576
[startup+500.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 15405 0 0 0 49959 46 0 0 25 0 1 0 358408678 66703360 15383 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16285 15383 603 41 0 16244 0
vsize: 65140
[startup+510.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 15863 0 0 0 50957 48 0 0 25 0 1 0 358408678 68579328 15841 4294967295 134512640 134672761 3221224560 3221223664 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16743 15841 603 41 0 16702 0
vsize: 66972
[startup+520.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 16308 0 0 0 51956 50 0 0 25 0 1 0 358408678 70324224 16286 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17169 16286 603 41 0 17128 0
vsize: 68676
[startup+530.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 16680 0 0 0 52954 51 0 0 25 0 1 0 358408678 71938048 16658 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17563 16658 603 41 0 17522 0
vsize: 70252
[startup+540.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 17035 0 0 0 53954 52 0 0 25 0 1 0 358408678 73273344 17013 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17889 17013 603 41 0 17848 0
vsize: 71556
[startup+550.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 17328 0 0 0 54953 53 0 0 25 0 1 0 358408678 74473472 17306 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18182 17306 603 41 0 18141 0
vsize: 72728
[startup+560.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 17674 0 0 0 55952 54 0 0 25 0 1 0 358408678 75943936 17652 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18541 17652 603 41 0 18500 0
vsize: 74164
[startup+570.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 17985 0 0 0 56952 55 0 0 25 0 1 0 358408678 77144064 17963 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18834 17963 603 41 0 18793 0
vsize: 75336
[startup+580.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 18332 0 0 0 57951 56 0 0 25 0 1 0 358408678 78622720 18310 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19195 18310 603 41 0 19154 0
vsize: 76780
[startup+590.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 18629 0 0 0 58950 57 0 0 25 0 1 0 358408678 79822848 18607 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19488 18607 603 41 0 19447 0
vsize: 77952
[startup+600.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 18941 0 0 0 59948 59 0 0 25 0 1 0 358408678 81031168 18919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19783 18919 603 41 0 19742 0
vsize: 79132
[startup+610.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 19284 0 0 0 60947 60 0 0 25 0 1 0 358408678 82497536 19262 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20141 19262 603 41 0 20100 0
vsize: 80564
[startup+620.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 19528 0 0 0 61946 61 0 0 25 0 1 0 358408678 83562496 19506 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20401 19506 603 41 0 20360 0
vsize: 81604
[startup+630.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 19797 0 0 0 62946 62 0 0 25 0 1 0 358408678 84635648 19775 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20663 19775 603 41 0 20622 0
vsize: 82652
[startup+640.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 20034 0 0 0 63945 63 0 0 25 0 1 0 358408678 85573632 20012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20892 20012 603 41 0 20851 0
vsize: 83568
[startup+650.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 20291 0 0 0 64944 64 0 0 25 0 1 0 358408678 86654976 20269 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21156 20269 603 41 0 21115 0
vsize: 84624
[startup+660.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 20544 0 0 0 65943 65 0 0 25 0 1 0 358408678 87584768 20522 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21383 20522 603 41 0 21342 0
vsize: 85532
[startup+670.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 20805 0 0 0 66942 66 0 0 25 0 1 0 358408678 88653824 20783 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21644 20783 603 41 0 21603 0
vsize: 86576
[startup+680.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3781
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 21111 0 0 0 67941 67 0 0 25 0 1 0 358408678 89989120 21089 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21970 21089 603 41 0 21929 0
vsize: 87880
[startup+690.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 21440 0 0 0 68940 68 0 0 25 0 1 0 358408678 91324416 21418 4294967295 134512640 134672761 3221224560 3221223744 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22296 21418 603 41 0 22255 0
vsize: 89184
[startup+700.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 21746 0 0 0 69939 69 0 0 25 0 1 0 358408678 92520448 21724 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21724 603 41 0 22547 0
vsize: 90352
[startup+710.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 22077 0 0 0 70938 70 0 0 25 0 1 0 358408678 93855744 22055 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22914 22055 603 41 0 22873 0
vsize: 91656
[startup+720.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 22404 0 0 0 71937 71 0 0 25 0 1 0 358408678 95182848 22382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23238 22382 603 41 0 23197 0
vsize: 92952
[startup+730.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 22729 0 0 0 72937 72 0 0 25 0 1 0 358408678 97042432 22707 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23692 22707 603 41 0 23651 0
vsize: 94768
[startup+740.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 23063 0 0 0 73935 73 0 0 25 0 1 0 358408678 98357248 23041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24013 23041 603 41 0 23972 0
vsize: 96052
[startup+750.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 23415 0 0 0 74935 74 0 0 25 0 1 0 358408678 99823616 23393 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24371 23393 603 41 0 24330 0
vsize: 97484
[startup+760.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 23734 0 0 0 75934 76 0 0 25 0 1 0 358408678 101134336 23712 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24691 23712 603 41 0 24650 0
vsize: 98764
[startup+770.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 24019 0 0 0 76933 77 0 0 25 0 1 0 358408678 102318080 23997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24980 23997 603 41 0 24939 0
vsize: 99920
[startup+780.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 24288 0 0 0 77932 78 0 0 25 0 1 0 358408678 103391232 24266 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25242 24266 603 41 0 25201 0
vsize: 100968
[startup+790.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 24552 0 0 0 78931 79 0 0 25 0 1 0 358408678 104464384 24530 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25504 24530 603 41 0 25463 0
vsize: 102016
[startup+800.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 24773 0 0 0 79930 80 0 0 25 0 1 0 358408678 105402368 24751 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25733 24751 603 41 0 25692 0
vsize: 102932
[startup+810.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 25055 0 0 0 80929 81 0 0 25 0 1 0 358408678 106618880 25033 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26030 25033 603 41 0 25989 0
vsize: 104120
[startup+820.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 25274 0 0 0 81929 82 0 0 25 0 1 0 358408678 107421696 25252 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26226 25252 603 41 0 26185 0
vsize: 104904
[startup+830.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 25557 0 0 0 82928 82 0 0 25 0 1 0 358408678 108621824 25535 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26519 25535 603 41 0 26478 0
vsize: 106076
[startup+840.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 25723 0 0 0 83928 83 0 0 25 0 1 0 358408678 109289472 25701 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26682 25701 603 41 0 26641 0
vsize: 106728
[startup+850.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 26004 0 0 0 84927 84 0 0 25 0 1 0 358408678 110489600 25982 4294967295 134512640 134672761 3221224560 3221223744 134558923 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26975 25982 603 41 0 26934 0
vsize: 107900
[startup+860.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 26303 0 0 0 85926 85 0 0 25 0 1 0 358408678 111689728 26281 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27268 26281 603 41 0 27227 0
vsize: 109072
[startup+870.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 26548 0 0 0 86926 85 0 0 25 0 1 0 358408678 112635904 26526 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27499 26526 603 41 0 27458 0
vsize: 109996
[startup+880.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 26800 0 0 0 87925 86 0 0 25 0 1 0 358408678 113700864 26778 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27759 26778 603 41 0 27718 0
vsize: 111036
[startup+890.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 27051 0 0 0 88925 86 0 0 25 0 1 0 358408678 114634752 27029 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27987 27029 603 41 0 27946 0
vsize: 111948
[startup+900.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 27293 0 0 0 89924 87 0 0 25 0 1 0 358408678 115712000 27271 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28250 27271 603 41 0 28209 0
vsize: 113000
[startup+910.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 27567 0 0 0 90923 88 0 0 25 0 1 0 358408678 116785152 27545 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28512 27545 603 41 0 28471 0
vsize: 114048
[startup+920.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 27794 0 0 0 91923 89 0 0 25 0 1 0 358408678 117714944 27772 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28739 27772 603 41 0 28698 0
vsize: 114956
[startup+930.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28034 0 0 0 92922 89 0 0 25 0 1 0 358408678 118644736 28012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28966 28012 603 41 0 28925 0
vsize: 115864
[startup+940.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28301 0 0 0 93921 90 0 0 25 0 1 0 358408678 119836672 28279 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29257 28279 603 41 0 29216 0
vsize: 117028
[startup+950.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28531 0 0 0 94921 91 0 0 25 0 1 0 358408678 120766464 28509 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29484 28509 603 41 0 29443 0
vsize: 117936
[startup+960.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28796 0 0 0 95920 92 0 0 25 0 1 0 358408678 121827328 28774 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29743 28774 603 41 0 29702 0
vsize: 118972
[startup+970.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 96920 92 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+980.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 97920 93 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+990.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 98920 93 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 99920 93 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 100920 93 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 101920 93 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 102920 93 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 103920 94 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 104920 94 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 105920 94 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 106920 94 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 107920 94 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 108920 94 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28941 0 0 0 109920 95 0 0 25 0 1 0 358408678 122363904 28919 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28919 603 41 0 29833 0
vsize: 119496
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 110920 95 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 111920 95 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 112920 95 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 113920 95 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 114920 95 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 115920 95 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 116920 95 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 117920 96 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 118920 96 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3783
Raw data (stat): 3724 (minisat+) R 3723 30927 30926 0 -1 0 28942 0 0 0 119920 96 0 0 25 0 1 0 358408678 122363904 28920 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28920 603 41 0 29833 0
vsize: 119496
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 3783
Raw data (stat): 3724 (minisat+) Z 3723 30927 30926 0 -1 12 28945 0 0 0 119920 101 0 0 25 0 1 0 358408678 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.1
CPU time (s): 1200.22
CPU user time (s): 1199.21
CPU system time (s): 1.01684
CPU usage (%): 100.011
Max. virtual memory (Kb): 119496
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####