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 6380

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        889464 kB
Buffers:         35036 kB
Cached:          88152 kB
SwapCached:       2272 kB
Active:          58184 kB
Inactive:        70156 kB
HighTotal:      131008 kB
HighFree:        38892 kB
LowTotal:       903652 kB
LowFree:        850572 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11156 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:06:05 (client local time) WITH STATUS 10 IN 1200.83 SECONDS
stats: 4847 7 1200.83 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 |  217187   480682 |   72395       0        0     nan |  0.000 % |
c |       100 |  217187   480682 |   79634     100     1501    15.0 |  0.015 % |
c |       250 |  216553   479257 |   87597     238     2260     9.5 |  0.377 % |
c |       475 |  214403   474331 |   96357     417     3370     8.1 |  1.779 % |
c |       813 |  208732   461312 |  105993     678     4911     7.2 |  5.522 % |
c |      1319 |  203181   448615 |  116592    1079     8100     7.5 |  9.102 % |
c |      2080 |  191853   422503 |  128252    1626    12734     7.8 | 16.792 % |
c |      3219 |  180100   395270 |  141077    2395    20901     8.7 | 25.008 % |
c |      4927 |  160484   349732 |  155185    3506    34149     9.7 | 38.786 % |
c |      7489 |  139045   299594 |  170703    4992    50079    10.0 | 54.097 % |
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 |      9443 |  128040   273852 |   42680    5940    60822    10.2 | 54.097 % |
c |      9543 |  127309   272135 |   46948    5955    61055    10.3 | 62.862 % |
c |      9693 |  126439   270108 |   51642    6075    62996    10.4 | 63.582 % |
c |      9918 |  126290   269767 |   56807    6299    66140    10.5 | 63.582 % |
c |     10256 |  123903   264151 |   62487    6373    66006    10.4 | 65.563 % |
c |     10762 |  117872   249966 |   68736    6356    66254    10.4 | 69.774 % |
c |     11522 |  117082   248089 |   75610    6996    71751    10.3 | 70.383 % |
c |     12661 |  113031   238586 |   83171    7487    78755    10.5 | 73.424 % |
c |     14369 |  108372   227649 |   91488    8599    95949    11.2 | 76.966 % |
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 |     15066 |  106698   223679 |   35566    8964   100189    11.2 | 76.966 % |
c |     15166 |  106660   223591 |   39122    9049   100980    11.2 | 78.228 % |
c |     15318 |  106307   222758 |   43034    9078   101276    11.2 | 78.498 % |
c |     15543 |  105826   221622 |   47338    9173   103205    11.3 | 78.877 % |
c |     15880 |  103570   216306 |   52072    8860   100198    11.3 | 80.589 % |
c |     16386 |  102870   214658 |   57279    9090   106633    11.7 | 81.121 % |
c |     17145 |  101626   211726 |   63007    9396   119714    12.7 | 82.054 % |
c |     18284 |  100289   208582 |   69308   10071   136639    13.6 | 83.059 % |
c ==============================================================================
c [1mFound solution: -39[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 |     19414 |   99722   207279 |   33240   11015   184717    16.8 | 83.059 % |
c |     19514 |   99638   207077 |   36564   11091   186417    16.8 | 83.630 % |
c |     19665 |   99638   207077 |   40220   11242   190040    16.9 | 83.630 % |
c |     19890 |   99630   207058 |   44242   11449   195514    17.1 | 83.636 % |
c |     20227 |   99399   206517 |   48666   11624   198852    17.1 | 83.811 % |
c |     20733 |   99074   205757 |   53533   11956   206585    17.3 | 84.046 % |
c |     21492 |   98984   205541 |   58886   12680   227936    18.0 | 84.122 % |
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 |     21935 |   98363   204070 |   32787   12660   224415    17.7 | 84.122 % |
c |     22035 |   98357   204056 |   36065   12747   225203    17.7 | 84.593 % |
c |     22185 |   98079   203394 |   39672   12739   224457    17.6 | 84.817 % |
c |     22410 |   97973   203145 |   43639   12822   227086    17.7 | 84.897 % |
c |     22748 |   97913   203000 |   48003   13131   238273    18.1 | 84.949 % |
c |     23254 |   97819   202777 |   52803   13555   250809    18.5 | 85.022 % |
c |     24013 |   97616   202297 |   58084   14145   263682    18.6 | 85.184 % |
c |     25152 |   97610   202283 |   63892   15274   316969    20.8 | 85.188 % |
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 |     26630 |   97403   201804 |   32467   16570   365654    22.1 | 85.188 % |
c |     26730 |   97379   201749 |   35713   16586   367504    22.2 | 85.400 % |
c |     26881 |   97375   201740 |   39285   16736   369250    22.1 | 85.402 % |
c |     27106 |   97361   201707 |   43213   16954   374430    22.1 | 85.413 % |
c |     27443 |   97293   201546 |   47534   17193   384899    22.4 | 85.467 % |
c |     27949 |   97281   201518 |   52288   17693   397205    22.4 | 85.475 % |
c |     28708 |   97187   201297 |   57517   18384   434405    23.6 | 85.546 % |
c |     29847 |   97000   200866 |   63268   19343   469225    24.3 | 85.674 % |
c |     31555 |   96220   199029 |   69595   20491   558102    27.2 | 86.288 % |
c |     34117 |   96180   198935 |   76555   22977   771684    33.6 | 86.318 % |
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 |     34807 |   96139   198821 |   32046   23629   843306    35.7 | 86.318 % |
c |     34907 |   96039   198586 |   35250   23541   842209    35.8 | 86.407 % |
c |     35057 |   96039   198586 |   38775   23691   853577    36.0 | 86.407 % |
c |     35282 |   96039   198586 |   42653   23916   861422    36.0 | 86.407 % |
c |     35619 |   96039   198586 |   46918   24253   884420    36.5 | 86.407 % |
c |     36126 |   96029   198562 |   51610   24690   901432    36.5 | 86.416 % |
c |     36888 |   95812   198043 |   56771   24964   931898    37.3 | 86.595 % |
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 |     37563 |   95898   198260 |   31966   25639   969849    37.8 | 86.595 % |
c |     37664 |   95884   198226 |   35162   25674   971039    37.8 | 86.582 % |
c |     37815 |   95884   198226 |   38678   25825   980193    38.0 | 86.582 % |
c |     38040 |   95884   198226 |   42546   26050   995264    38.2 | 86.582 % |
c |     38377 |   95880   198217 |   46801   26386  1011481    38.3 | 86.585 % |
c |     38884 |   95880   198217 |   51481   26893  1051848    39.1 | 86.585 % |
c |     39644 |   95880   198217 |   56629   27653  1099255    39.8 | 86.585 % |
c |     40784 |   95789   198005 |   62292   28693  1218845    42.5 | 86.651 % |
c |     42493 |   95714   197826 |   68521   30287  1381711    45.6 | 86.714 % |
c |     45056 |   95714   197826 |   75374   32850  1766727    53.8 | 86.714 % |
c |     48900 |   95403   197104 |   82911   36295  2122238    58.5 | 86.935 % |
c |     54666 |   95272   196795 |   91202   42016  2785354    66.3 | 87.039 % |
c |     63315 |   95272   196795 |  100323   50665  3947094    77.9 | 87.039 % |
c |     76291 |   95238   196715 |  110355   63493  5613142    88.4 | 87.064 % |
c |     95752 |   95238   196715 |  121390   82954  9070324   109.3 | 87.064 % |
c |    124944 |   94850   195801 |  133529  111976 12934315   115.5 | 87.366 % |
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 |    129638 |   94764   195586 |   31588  116186 13312212   114.6 | 87.366 % |
c |    129738 |   94732   195510 |   34746   23087  1566712    67.9 | 87.448 % |
c |    129889 |   94732   195510 |   38221   23238  1571895    67.6 | 87.448 % |
c |    130115 |   94732   195510 |   42043   23464  1588799    67.7 | 87.448 % |
c |    130452 |   94732   195510 |   46247   23801  1640507    68.9 | 87.448 % |
c |    130958 |   94732   195510 |   50872   24307  1690503    69.5 | 87.448 % |
c |    131717 |   94718   195477 |   55960   25054  1788643    71.4 | 87.459 % |
c |    132857 |   94718   195477 |   61556   26194  1893520    72.3 | 87.459 % |
c |    134565 |   94636   195284 |   67711   27884  2063236    74.0 | 87.521 % |
c |    137127 |   94636   195284 |   74482   30446  2362358    77.6 | 87.521 % |
c |    140971 |   94630   195270 |   81931   34287  2906974    84.8 | 87.525 % |
c |    146737 |   94630   195270 |   90124   40053  3834122    95.7 | 87.525 % |
c |    155387 |   94564   195113 |   99136   48678  4774540    98.1 | 87.579 % |
c |    168361 |   94457   194862 |  109050   61646  6482959   105.2 | 87.661 % |
c |    187822 |   94303   194506 |  119955   81095  8939241   110.2 | 87.771 % |
c |    217014 |   94243   194364 |  131950  110258 13333937   120.9 | 87.818 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    231036 |   94290   194481 |   31430  124280 14968785   120.4 | 87.818 % |
c |    231137 |   94290   194481 |   34573   21200  1574263    74.3 | 87.795 % |
c |    231287 |   94290   194481 |   38030   21350  1581228    74.1 | 87.795 % |
c |    231512 |   94290   194481 |   41833   21575  1590584    73.7 | 87.795 % |
c |    231850 |   94290   194481 |   46016   21913  1602211    73.1 | 87.795 % |
c |    232357 |   94194   194257 |   50618   22403  1631666    72.8 | 87.866 % |
c |    233116 |   94158   194171 |   55680   23149  1696465    73.3 | 87.896 % |
c |    234257 |   94158   194171 |   61248   24290  1766094    72.7 | 87.896 % |
c |    235966 |   94158   194171 |   67372   25999  1918027    73.8 | 87.896 % |
c |    238528 |   94158   194171 |   74110   28561  2158330    75.6 | 87.896 % |
c |    242373 |   94144   194137 |   81521   32400  2585802    79.8 | 87.909 % |
c |    248139 |   94031   193873 |   89673   38159  3196499    83.8 | 87.993 % |
c |    256788 |   94023   193854 |   98640   46805  4229182    90.4 | 87.999 % |
c |    269762 |   94023   193854 |  108504   59779  5705540    95.4 | 87.999 % |
c |    289223 |   93765   193254 |  119355   79214  8199825   103.5 | 88.182 % |
c |    318415 |   93747   193212 |  131290  108394 12475142   115.1 | 88.195 % |
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.84 0.94 0.90 2/54 29605
Raw data (stat): 29605 (runsolver) R 29604 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423597004 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5259 0 0 0 982 16 0 0 25 0 1 0 423597004 24322048 5237 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5938 5237 603 41 0 5897 0
vsize: 23752
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5266 0 0 0 1982 17 0 0 25 0 1 0 423597004 24322048 5244 4294967295 134512640 134672761 3221224560 3221223696 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5938 5244 603 41 0 5897 0
vsize: 23752
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5271 0 0 0 2981 17 0 0 25 0 1 0 423597004 24322048 5249 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5938 5249 603 41 0 5897 0
vsize: 23752
[startup+40.0022 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5276 0 0 0 3981 17 0 0 25 0 1 0 423597004 24457216 5254 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5971 5254 603 41 0 5930 0
vsize: 23884
[startup+50.003 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5278 0 0 0 4981 18 0 0 25 0 1 0 423597004 24457216 5256 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5971 5256 603 41 0 5930 0
vsize: 23884
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5284 0 0 0 5981 18 0 0 25 0 1 0 423597004 24457216 5262 4294967295 134512640 134672761 3221224560 3221223732 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5971 5262 603 41 0 5930 0
vsize: 23884
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5286 0 0 0 6980 18 0 0 25 0 1 0 423597004 24457216 5264 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5971 5264 603 41 0 5930 0
vsize: 23884
[startup+80.0034 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5559 0 0 0 7980 19 0 0 25 0 1 0 423597004 26464256 5537 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6461 5537 603 41 0 6420 0
vsize: 25844
[startup+90.0041 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5559 0 0 0 8980 19 0 0 25 0 1 0 423597004 26464256 5537 4294967295 134512640 134672761 3221224560 3221223728 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6461 5537 603 41 0 6420 0
vsize: 25844
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5560 0 0 0 9980 19 0 0 25 0 1 0 423597004 26464256 5538 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5538 603 41 0 6420 0
vsize: 25844
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 5771 0 0 0 10978 19 0 0 25 0 1 0 423597004 27324416 5749 4294967295 134512640 134672761 3221224560 3221223744 134559594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6671 5749 603 41 0 6630 0
vsize: 26684
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 6270 0 0 0 11976 22 0 0 25 0 1 0 423597004 29368320 6248 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7170 6248 603 41 0 7129 0
vsize: 28680
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 6693 0 0 0 12975 23 0 0 25 0 1 0 423597004 31035392 6671 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7577 6671 603 41 0 7536 0
vsize: 30308
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 7300 0 0 0 13972 26 0 0 25 0 1 0 423597004 33714176 7278 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8231 7278 603 41 0 8190 0
vsize: 32924
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 7792 0 0 0 14971 27 0 0 25 0 1 0 423597004 35717120 7770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8720 7770 603 41 0 8679 0
vsize: 34880
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 8353 0 0 0 15969 29 0 0 25 0 1 0 423597004 38010880 8331 4294967295 134512640 134672761 3221224560 3221223744 134559594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9280 8331 603 41 0 9239 0
vsize: 37120
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 9049 0 0 0 16966 32 0 0 25 0 1 0 423597004 40812544 9027 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9964 9027 603 41 0 9923 0
vsize: 39856
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 9505 0 0 0 17965 34 0 0 25 0 1 0 423597004 42692608 9483 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10423 9483 603 41 0 10382 0
vsize: 41692
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 9909 0 0 0 18964 35 0 0 25 0 1 0 423597004 44302336 9887 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10816 9887 603 41 0 10775 0
vsize: 43264
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 10352 0 0 0 19962 37 0 0 25 0 1 0 423597004 46039040 10330 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11240 10330 603 41 0 11199 0
vsize: 44960
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 10848 0 0 0 20961 39 0 0 25 0 1 0 423597004 48041984 10826 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11729 10826 603 41 0 11688 0
vsize: 46916
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 11273 0 0 0 21959 40 0 0 25 0 1 0 423597004 49778688 11251 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12153 11251 603 41 0 12112 0
vsize: 48612
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 11751 0 0 0 22958 41 0 0 25 0 1 0 423597004 52043776 11729 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12706 11729 603 41 0 12665 0
vsize: 50824
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 12268 0 0 0 23957 42 0 0 25 0 1 0 423597004 54169600 12246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13225 12246 603 41 0 13184 0
vsize: 52900
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 12717 0 0 0 24957 44 0 0 25 0 1 0 423597004 55918592 12695 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13652 12695 603 41 0 13611 0
vsize: 54608
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 13166 0 0 0 25955 45 0 0 25 0 1 0 423597004 57782272 13144 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14107 13144 603 41 0 14066 0
vsize: 56428
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 13640 0 0 0 26954 46 0 0 25 0 1 0 423597004 59785216 13618 4294967295 134512640 134672761 3221224560 3221223744 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14596 13618 603 41 0 14555 0
vsize: 58384
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 14076 0 0 0 27954 47 0 0 25 0 1 0 423597004 61497344 14054 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15014 14054 603 41 0 14973 0
vsize: 60056
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 14466 0 0 0 28953 48 0 0 25 0 1 0 423597004 63107072 14444 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15407 14444 603 41 0 15366 0
vsize: 61628
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 14891 0 0 0 29952 49 0 0 25 0 1 0 423597004 64843776 14869 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15831 14869 603 41 0 15790 0
vsize: 63324
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 15158 0 0 0 30951 50 0 0 25 0 1 0 423597004 65912832 15136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16092 15136 603 41 0 16051 0
vsize: 64368
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 15543 0 0 0 31950 51 0 0 25 0 1 0 423597004 67514368 15521 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16483 15521 603 41 0 16442 0
vsize: 65932
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 15955 0 0 0 32949 52 0 0 25 0 1 0 423597004 69099520 15933 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15933 603 41 0 16829 0
vsize: 67480
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 16331 0 0 0 33948 54 0 0 25 0 1 0 423597004 70705152 16309 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17262 16309 603 41 0 17221 0
vsize: 69048
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 16690 0 0 0 34947 55 0 0 25 0 1 0 423597004 72175616 16668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17621 16668 603 41 0 17580 0
vsize: 70484
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 17044 0 0 0 35945 57 0 0 25 0 1 0 423597004 73641984 17022 4294967295 134512640 134672761 3221224560 3221223696 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17979 17022 603 41 0 17938 0
vsize: 71916
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 17344 0 0 0 36944 58 0 0 25 0 1 0 423597004 74838016 17322 4294967295 134512640 134672761 3221224560 3221223664 134559802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18271 17322 603 41 0 18230 0
vsize: 73084
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 17670 0 0 0 37943 59 0 0 25 0 1 0 423597004 76169216 17648 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18596 17648 603 41 0 18555 0
vsize: 74384
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 17982 0 0 0 38943 60 0 0 25 0 1 0 423597004 77361152 17960 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18887 17960 603 41 0 18846 0
vsize: 75548
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 18315 0 0 0 39942 61 0 0 25 0 1 0 423597004 78704640 18293 4294967295 134512640 134672761 3221224560 3221223732 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19215 18293 603 41 0 19174 0
vsize: 76860
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 18617 0 0 0 40941 62 0 0 25 0 1 0 423597004 80039936 18595 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19541 18595 603 41 0 19500 0
vsize: 78164
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 18922 0 0 0 41941 62 0 0 25 0 1 0 423597004 81244160 18900 4294967295 134512640 134672761 3221224560 3221223664 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19835 18900 603 41 0 19794 0
vsize: 79340
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19190 0 0 0 42940 63 0 0 25 0 1 0 423597004 82321408 19168 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20098 19168 603 41 0 20057 0
vsize: 80392
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19429 0 0 0 43938 64 0 0 25 0 1 0 423597004 83247104 19407 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20324 19407 603 41 0 20283 0
vsize: 81296
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 44938 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 45938 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 46938 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 47938 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 48938 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 49939 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 50939 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 51939 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 52939 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 53939 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 54940 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 55940 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 56940 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 57940 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 58940 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 59941 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 60941 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 61941 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 62941 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 63941 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 64942 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 65942 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 66942 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 67942 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 68942 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 69942 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 70943 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 71943 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19581 0 0 0 72943 65 0 0 25 0 1 0 423597004 83857408 19559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20473 19559 603 41 0 20432 0
vsize: 81892
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 19836 0 0 0 73943 65 0 0 25 0 1 0 423597004 84922368 19814 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20733 19814 603 41 0 20692 0
vsize: 82932
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 20109 0 0 0 74942 66 0 0 25 0 1 0 423597004 86118400 20087 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21025 20087 603 41 0 20984 0
vsize: 84100
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 20374 0 0 0 75941 67 0 0 25 0 1 0 423597004 87171072 20352 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21282 20352 603 41 0 21241 0
vsize: 85128
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 20617 0 0 0 76941 68 0 0 25 0 1 0 423597004 88113152 20595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21512 20595 603 41 0 21471 0
vsize: 86048
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 20848 0 0 0 77940 68 0 0 25 0 1 0 423597004 89038848 20826 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21738 20826 603 41 0 21697 0
vsize: 86952
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21161 0 0 0 78940 69 0 0 25 0 1 0 423597004 90374144 21139 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22064 21139 603 41 0 22023 0
vsize: 88256
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21437 0 0 0 79939 70 0 0 25 0 1 0 423597004 91447296 21415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22326 21415 603 41 0 22285 0
vsize: 89304
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 80938 70 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 81939 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 82939 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223664 134559796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+840.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29605
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 83950 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+850.405 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 29653
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 84978 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+860.407 s]
Raw data (loadavg): 1.21 1.02 0.93 2/54 29658
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 85976 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223760 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+870.661 s]
Raw data (loadavg): 1.18 1.02 0.93 2/54 29658
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 87001 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+880.661 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 29658
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 88002 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223696 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+890.66 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 29658
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 89002 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+900.66 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 29658
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 90002 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+910.66 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 29658
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 91002 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+920.661 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 92002 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+930.661 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 93002 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+940.661 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 94003 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+950.662 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 95003 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+960.662 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 96003 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+970.662 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 97003 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+980.661 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 98003 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+990.661 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 99003 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1000.66 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 100003 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1010.66 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 101004 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1020.66 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 102004 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1030.66 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 103004 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1040.66 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 104004 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1050.66 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 105004 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1060.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 106004 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1070.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 107005 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1080.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 108005 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1090.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 109005 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1100.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 110005 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1110.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 111005 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1120.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 112005 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1130.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 113005 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1140.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 114005 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1150.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 115006 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1160.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21500 0 0 0 116006 71 0 0 25 0 1 0 423597004 91688960 21478 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21478 603 41 0 22344 0
vsize: 89540
[startup+1170.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29660
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21501 0 0 0 117006 71 0 0 25 0 1 0 423597004 91688960 21479 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22385 21479 603 41 0 22344 0
vsize: 89540
[startup+1180.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29662
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21594 0 0 0 118006 71 0 0 25 0 1 0 423597004 92094464 21572 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22484 21572 603 41 0 22443 0
vsize: 89936
[startup+1190.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29662
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 21861 0 0 0 119006 72 0 0 25 0 1 0 423597004 93163520 21839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22745 21839 603 41 0 22704 0
vsize: 90980
[startup+1200.66 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29662
Raw data (stat): 29605 (minisat+) R 29604 24215 24214 0 -1 0 22142 0 0 0 120005 73 0 0 25 0 1 0 423597004 94883840 22120 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23165 22120 603 41 0 23124 0
vsize: 92660
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.71 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 29662
Raw data (stat): 29605 (minisat+) Z 29604 24215 24214 0 -1 12 22146 0 0 0 120005 77 0 0 25 0 1 0 423597004 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.71
CPU time (s): 1200.83
CPU user time (s): 1200.05
CPU system time (s): 0.775882
CPU usage (%): 100.01
Max. virtual memory (Kb): 92660
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####