PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        886088 kB
Buffers:         35072 kB
Cached:          70340 kB
SwapCached:        192 kB
Active:          55664 kB
Inactive:        52812 kB
HighTotal:      131008 kB
HighFree:        56812 kB
LowTotal:       903652 kB
LowFree:        829276 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34576 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:03:02 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4841 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 59186 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 |   59186   118372 |   19728       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  150827   332894 |   50275       0        0     nan |  0.000 % |
c |       101 |  150827   332894 |   55302     101     1177    11.7 |  0.004 % |
c |       251 |  150827   332894 |   60832     251     2269     9.0 |  0.003 % |
c |       476 |  147347   324910 |   66916     371     2877     7.8 |  3.423 % |
c |       813 |  143701   316572 |   73607     551     4358     7.9 |  6.931 % |
c |      1319 |  139246   306371 |   80968     942     7605     8.1 | 11.245 % |
c |      2078 |  131749   289118 |   89065    1513    13310     8.8 | 18.753 % |
c ==============================================================================
c [1mFound solution: -32[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 |      2247 |  130076   285260 |   43358    1644    14350     8.7 | 18.753 % |
c |      2347 |  128900   282557 |   47693    1723    14901     8.6 | 21.539 % |
c |      2497 |  127294   278827 |   52463    1828    15669     8.6 | 23.191 % |
c |      2722 |  126284   276481 |   57709    2012    18055     9.0 | 24.233 % |
c |      3059 |  123919   270950 |   63480    2242    20023     8.9 | 26.718 % |
c |      3565 |  119285   260211 |   69828    2574    22480     8.7 | 31.423 % |
c |      4324 |  112299   244015 |   76811    3040    27820     9.2 | 38.661 % |
c |      5463 |  105488   228139 |   84492    3754    34918     9.3 | 45.900 % |
c ==============================================================================
c [1mFound solution: -33[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 |      5681 |  104317   225438 |   34772    3906    36455     9.3 | 45.900 % |
c |      5781 |  103581   223715 |   38249    3936    36965     9.4 | 48.073 % |
c |      5931 |  102931   222200 |   42074    4050    37861     9.3 | 48.775 % |
c ==============================================================================
c [1mFound solution: -34[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 |      6134 |  100990   217604 |   33663    4153    39065     9.4 | 48.775 % |
c |      6235 |  100788   217133 |   37029    4242    39663     9.4 | 50.992 % |
c |      6385 |   99805   214838 |   40732    4262    39950     9.4 | 52.068 % |
c |      6611 |   99344   213747 |   44805    4444    41672     9.4 | 52.577 % |
c |      6948 |   97642   209793 |   49285    4672    44848     9.6 | 54.346 % |
c |      7454 |   92879   198623 |   54214    4627    45659     9.9 | 59.591 % |
c ==============================================================================
c [1mFound solution: -35[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 |      8150 |   91382   195181 |   30460    5149    53033    10.3 | 59.591 % |
c |      8250 |   91289   194962 |   33506    5248    54077    10.3 | 61.544 % |
c |      8400 |   90506   193129 |   36856    5317    56481    10.6 | 62.409 % |
c |      8625 |   89386   190497 |   40542    5376    57917    10.8 | 63.644 % |
c |      8963 |   87967   187165 |   44596    5600    61652    11.0 | 65.209 % |
c |      9469 |   85878   182264 |   49056    5890    65880    11.2 | 67.514 % |
c |     10228 |   83593   176875 |   53961    6345    73770    11.6 | 70.042 % |
c |     11367 |   79519   167286 |   59357    6766    86576    12.8 | 74.575 % |
c |     13075 |   75923   158816 |   65293    7738   111109    14.4 | 78.649 % |
c ==============================================================================
c [1mFound solution: -36[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 |     14330 |   74757   156044 |   24919    8728   131183    15.0 | 78.649 % |
c |     14430 |   74576   155612 |   27410    8810   131692    14.9 | 80.224 % |
c |     14580 |   74419   155246 |   30151    8917   132632    14.9 | 80.313 % |
c |     14807 |   74098   154499 |   33167    9055   136039    15.0 | 80.649 % |
c |     15146 |   74098   154499 |   36483    9394   146978    15.6 | 80.649 % |
c |     15652 |   73868   153960 |   40132    9725   158156    16.3 | 80.898 % |
c |     16411 |   73808   153818 |   44145   10415   217201    20.9 | 80.968 % |
c |     17550 |   73303   152612 |   48560   11429   247726    21.7 | 81.574 % |
c |     19258 |   73181   152322 |   53416   13056   321930    24.7 | 81.712 % |
c |     21821 |   72985   151858 |   58757   15536   500219    32.2 | 81.938 % |
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 |     23782 |   72779   151387 |   24259   17353   608381    35.1 | 81.938 % |
c |     23882 |   72583   150927 |   26684   17360   609626    35.1 | 82.444 % |
c |     24032 |   72583   150927 |   29353   17510   613680    35.0 | 82.444 % |
c |     24257 |   72569   150894 |   32288   17726   620219    35.0 | 82.460 % |
c |     24594 |   72374   150432 |   35517   18013   635849    35.3 | 82.692 % |
c |     25100 |   71975   149488 |   39069   18363   649775    35.4 | 83.155 % |
c |     25859 |   71959   149451 |   42976   19108   711337    37.2 | 83.171 % |
c |     26999 |   71959   149451 |   47273   20248   798920    39.5 | 83.171 % |
c |     28709 |   71566   148514 |   52001   21560   970792    45.0 | 83.643 % |
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 |     30894 |   71522   148387 |   23840   23692  1198092    50.6 | 83.643 % |
c |     30994 |   71522   148387 |   26224   23792  1201255    50.5 | 83.669 % |
c |     31145 |   71484   148297 |   28846   23898  1208396    50.6 | 83.714 % |
c |     31370 |   71478   148283 |   31731   24122  1217118    50.5 | 83.720 % |
c |     31707 |   71379   148050 |   34904   24234  1233158    50.9 | 83.835 % |
c |     32213 |   71344   147969 |   38394   24738  1244859    50.3 | 83.873 % |
c |     32973 |   71336   147950 |   42234   25493  1292842    50.7 | 83.883 % |
c |     34112 |   71318   147907 |   46457   26615  1382218    51.9 | 83.905 % |
c |     35821 |   71232   147704 |   51103   28239  1517690    53.7 | 84.001 % |
c |     38383 |   71232   147704 |   56213   30801  1711690    55.6 | 84.001 % |
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 |     42070 |   71309   147900 |   23769   34488  2121047    61.5 | 84.001 % |
c |     42170 |   71309   147900 |   26145   34588  2130759    61.6 | 83.993 % |
c |     42320 |   71309   147900 |   28760   34738  2140344    61.6 | 83.993 % |
c |     42545 |   71309   147900 |   31636   34963  2153036    61.6 | 83.993 % |
c |     42882 |   71273   147813 |   34800   35270  2171702    61.6 | 84.041 % |
c |     43388 |   71273   147813 |   38280   35776  2208813    61.7 | 84.041 % |
c |     44147 |   71273   147813 |   42108   36535  2273844    62.2 | 84.041 % |
c |     45286 |   71118   147450 |   46319   37391  2341966    62.6 | 84.216 % |
c |     46994 |   71118   147450 |   50950   39099  2458629    62.9 | 84.216 % |
c |     49556 |   71047   147283 |   56046   41628  2699920    64.9 | 84.298 % |
c |     53401 |   71041   147269 |   61650   45465  3223627    70.9 | 84.305 % |
c |     59167 |   71041   147269 |   67815   51231  3913411    76.4 | 84.305 % |
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 |     65404 |   71007   147169 |   23669   57352  4479473    78.1 | 84.305 % |
c |     65504 |   70979   147102 |   26035   19053  1328882    69.7 | 84.369 % |
c |     65654 |   70979   147102 |   28639   19203  1332108    69.4 | 84.369 % |
c |     65879 |   70979   147102 |   31503   19428  1336189    68.8 | 84.369 % |
c |     66216 |   70973   147088 |   34653   19762  1356738    68.7 | 84.375 % |
c |     66724 |   70973   147088 |   38119   20270  1411105    69.6 | 84.375 % |
c |     67483 |   70973   147088 |   41931   21029  1458802    69.4 | 84.375 % |
c |     68622 |   70963   147065 |   46124   22156  1552727    70.1 | 84.385 % |
c |     70330 |   70834   146758 |   50736   23836  1757115    73.7 | 84.541 % |
c |     72892 |   70834   146758 |   55810   26398  1998923    75.7 | 84.541 % |
c |     76736 |   70834   146758 |   61391   30242  2427651    80.3 | 84.541 % |
c |     82502 |   70685   146410 |   67530   35984  2971252    82.6 | 84.706 % |
c |     91152 |   70618   146253 |   74283   44624  3899023    87.4 | 84.782 % |
c |    104126 |   70549   146093 |   81711   57589  5205478    90.4 | 84.855 % |
c |    123587 |   70430   145816 |   89882   77033  8102759   105.2 | 84.982 % |
c |    152780 |   70278   145461 |   98871  106101 11558767   108.9 | 85.151 % |
c |    196569 |   69700   144093 |  108758   40445  4683924   115.8 | 85.821 % |
c |    262253 |   69700   144093 |  119634  106129 15123465   142.5 | 85.821 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 C715 C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 C592 -C591 -C590 -C589 -C588 -C587 C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 C268 -C267 -C266 -C265#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.91 2/54 8578
Raw data (stat): 8578 (runsolver) R 8577 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481798713 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.0002 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 3831 0 0 0 986 11 0 0 25 0 1 0 481798713 17678336 3809 4294967295 134512640 134672761 3221224560 3221223776 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4316 3809 603 41 0 4275 0
vsize: 17264
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 3950 0 0 0 1985 12 0 0 25 0 1 0 481798713 18522112 3928 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4522 3928 603 41 0 4481 0
vsize: 18088
[startup+30.0005 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 3950 0 0 0 2985 12 0 0 25 0 1 0 481798713 18522112 3928 4294967295 134512640 134672761 3221224560 3221223756 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4522 3928 603 41 0 4481 0
vsize: 18088
[startup+40.0001 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 3950 0 0 0 3985 12 0 0 25 0 1 0 481798713 18522112 3928 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4522 3928 603 41 0 4481 0
vsize: 18088
[startup+50.0007 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 3951 0 0 0 4985 12 0 0 25 0 1 0 481798713 18522112 3929 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4522 3929 603 41 0 4481 0
vsize: 18088
[startup+60.0005 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 4000 0 0 0 5985 12 0 0 25 0 1 0 481798713 18636800 3978 4294967295 134512640 134672761 3221224560 3221223664 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4550 3978 603 41 0 4509 0
vsize: 18200
[startup+70.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 4511 0 0 0 6983 14 0 0 25 0 1 0 481798713 20783104 4489 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5074 4489 603 41 0 5033 0
vsize: 20296
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 5100 0 0 0 7980 17 0 0 25 0 1 0 481798713 23203840 5078 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5665 5078 603 41 0 5624 0
vsize: 22660
[startup+90.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 5552 0 0 0 8979 18 0 0 25 0 1 0 481798713 25042944 5530 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6114 5530 603 41 0 6073 0
vsize: 24456
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 6122 0 0 0 9978 20 0 0 25 0 1 0 481798713 27447296 6100 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6701 6100 603 41 0 6660 0
vsize: 26804
[startup+110.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 6520 0 0 0 10976 21 0 0 25 0 1 0 481798713 29122560 6498 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7110 6498 603 41 0 7069 0
vsize: 28440
[startup+120.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 7020 0 0 0 11974 24 0 0 25 0 1 0 481798713 31133696 6998 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 6998 603 41 0 7560 0
vsize: 30404
[startup+130.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 7558 0 0 0 12973 25 0 0 25 0 1 0 481798713 33275904 7536 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8124 7536 603 41 0 8083 0
vsize: 32496
[startup+140.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8063 0 0 0 13970 28 0 0 25 0 1 0 481798713 35414016 8041 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8041 603 41 0 8605 0
vsize: 34584
[startup+150.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8430 0 0 0 14968 30 0 0 25 0 1 0 481798713 36888576 8408 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9006 8408 603 41 0 8965 0
vsize: 36024
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8749 0 0 0 15968 31 0 0 25 0 1 0 481798713 38088704 8727 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9299 8727 603 41 0 9258 0
vsize: 37196
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8749 0 0 0 16968 31 0 0 25 0 1 0 481798713 38088704 8727 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9299 8727 603 41 0 9258 0
vsize: 37196
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8749 0 0 0 17968 31 0 0 25 0 1 0 481798713 38088704 8727 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9299 8727 603 41 0 9258 0
vsize: 37196
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8749 0 0 0 18968 31 0 0 25 0 1 0 481798713 38088704 8727 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9299 8727 603 41 0 9258 0
vsize: 37196
[startup+199.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8749 0 0 0 19968 31 0 0 25 0 1 0 481798713 38088704 8727 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9299 8727 603 41 0 9258 0
vsize: 37196
[startup+209.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8749 0 0 0 20968 31 0 0 25 0 1 0 481798713 38088704 8727 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9299 8727 603 41 0 9258 0
vsize: 37196
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8749 0 0 0 21968 31 0 0 25 0 1 0 481798713 38088704 8727 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9299 8727 603 41 0 9258 0
vsize: 37196
[startup+229.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 8903 0 0 0 22968 32 0 0 25 0 1 0 481798713 38764544 8881 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9464 8882 603 41 0 9423 0
vsize: 37856
[startup+239.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 9249 0 0 0 23967 33 0 0 25 0 1 0 481798713 40226816 9227 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9821 9227 603 41 0 9780 0
vsize: 39284
[startup+249.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 9533 0 0 0 24966 34 0 0 25 0 1 0 481798713 41414656 9511 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10111 9511 603 41 0 10070 0
vsize: 40444
[startup+259.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 9874 0 0 0 25965 35 0 0 25 0 1 0 481798713 42745856 9852 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10436 9852 603 41 0 10395 0
vsize: 41744
[startup+269.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 10397 0 0 0 26964 37 0 0 25 0 1 0 481798713 44875776 10375 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10956 10375 603 41 0 10915 0
vsize: 43824
[startup+279.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 10783 0 0 0 27962 38 0 0 25 0 1 0 481798713 46743552 10761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11412 10761 603 41 0 11371 0
vsize: 45648
[startup+289.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 11200 0 0 0 28961 39 0 0 25 0 1 0 481798713 48353280 11178 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11805 11178 603 41 0 11764 0
vsize: 47220
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 11617 0 0 0 29960 40 0 0 25 0 1 0 481798713 50081792 11595 4294967295 134512640 134672761 3221224560 3221223664 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12227 11595 603 41 0 12186 0
vsize: 48908
[startup+309.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 12059 0 0 0 30959 42 0 0 25 0 1 0 481798713 51949568 12037 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12683 12037 603 41 0 12642 0
vsize: 50732
[startup+319.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 12437 0 0 0 31958 43 0 0 25 0 1 0 481798713 53403648 12415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13038 12415 603 41 0 12997 0
vsize: 52152
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 12747 0 0 0 32957 44 0 0 25 0 1 0 481798713 54734848 12725 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13363 12725 603 41 0 13322 0
vsize: 53452
[startup+339.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 13040 0 0 0 33956 46 0 0 25 0 1 0 481798713 55934976 13018 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13656 13018 603 41 0 13615 0
vsize: 54624
[startup+349.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 13312 0 0 0 34955 46 0 0 25 0 1 0 481798713 56991744 13290 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13914 13290 603 41 0 13873 0
vsize: 55656
[startup+359.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 13600 0 0 0 35954 47 0 0 25 0 1 0 481798713 58195968 13578 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14208 13578 603 41 0 14167 0
vsize: 56832
[startup+369.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 13881 0 0 0 36953 49 0 0 25 0 1 0 481798713 59265024 13859 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14469 13859 603 41 0 14428 0
vsize: 57876
[startup+379.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 14167 0 0 0 37952 50 0 0 25 0 1 0 481798713 60461056 14145 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14761 14145 603 41 0 14720 0
vsize: 59044
[startup+389.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 14447 0 0 0 38952 50 0 0 25 0 1 0 481798713 61648896 14425 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15051 14425 603 41 0 15010 0
vsize: 60204
[startup+399.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 14738 0 0 0 39952 51 0 0 25 0 1 0 481798713 62844928 14716 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15343 14716 603 41 0 15302 0
vsize: 61372
[startup+409.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 15034 0 0 0 40951 52 0 0 25 0 1 0 481798713 64049152 15012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15637 15012 603 41 0 15596 0
vsize: 62548
[startup+419.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 15304 0 0 0 41951 52 0 0 25 0 1 0 481798713 65101824 15282 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15894 15282 603 41 0 15853 0
vsize: 63576
[startup+429.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 15569 0 0 0 42950 54 0 0 25 0 1 0 481798713 66174976 15547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16156 15547 603 41 0 16115 0
vsize: 64624
[startup+439.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 15853 0 0 0 43949 55 0 0 25 0 1 0 481798713 67375104 15831 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16449 15831 603 41 0 16408 0
vsize: 65796
[startup+449.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 16180 0 0 0 44948 56 0 0 25 0 1 0 481798713 68710400 16158 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16775 16158 603 41 0 16734 0
vsize: 67100
[startup+459.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 16458 0 0 0 45946 57 0 0 25 0 1 0 481798713 69787648 16436 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17038 16436 603 41 0 16997 0
vsize: 68152
[startup+469.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 16770 0 0 0 46945 58 0 0 25 0 1 0 481798713 71135232 16748 4294967295 134512640 134672761 3221224560 3221223576 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17367 16748 603 41 0 17326 0
vsize: 69468
[startup+479.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 17088 0 0 0 47945 58 0 0 25 0 1 0 481798713 72335360 17066 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17660 17066 603 41 0 17619 0
vsize: 70640
[startup+489.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 17401 0 0 0 48944 59 0 0 25 0 1 0 481798713 73670656 17379 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17986 17379 603 41 0 17945 0
vsize: 71944
[startup+499.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 17672 0 0 0 49943 60 0 0 25 0 1 0 481798713 74735616 17650 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18246 17650 603 41 0 18205 0
vsize: 72984
[startup+509.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 17939 0 0 0 50943 61 0 0 25 0 1 0 481798713 75800576 17917 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18506 17917 603 41 0 18465 0
vsize: 74024
[startup+519.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 18206 0 0 0 51942 62 0 0 25 0 1 0 481798713 76996608 18184 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18798 18184 603 41 0 18757 0
vsize: 75192
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 18464 0 0 0 52942 63 0 0 25 0 1 0 481798713 77942784 18442 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19029 18442 603 41 0 18988 0
vsize: 76116
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 18687 0 0 0 53941 64 0 0 25 0 1 0 481798713 78888960 18665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 18665 603 41 0 19219 0
vsize: 77040
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 18926 0 0 0 54941 64 0 0 25 0 1 0 481798713 79810560 18904 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19485 18904 603 41 0 19444 0
vsize: 77940
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19176 0 0 0 55940 65 0 0 25 0 1 0 481798713 80879616 19154 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19746 19154 603 41 0 19705 0
vsize: 78984
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19403 0 0 0 56940 65 0 0 25 0 1 0 481798713 81809408 19381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19973 19381 603 41 0 19932 0
vsize: 79892
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 57940 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223360 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 58940 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 59940 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 60941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 61941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 62941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223696 134560652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 63941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 64941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 65941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 66941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 67941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 68941 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 69942 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 70942 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 71942 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 72942 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223664 134560231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 73942 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 74943 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 75943 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+770.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 76943 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 77943 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+790.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 78943 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 79944 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 80944 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+820.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 81944 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+830.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 82944 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 83944 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+850.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 84944 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 85945 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 86945 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 87945 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 88945 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223696 134560579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+900.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19632 0 0 0 89945 66 0 0 25 0 1 0 481798713 82743296 19610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 19610 603 41 0 20160 0
vsize: 80804
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 19908 0 0 0 90944 67 0 0 25 0 1 0 481798713 83943424 19886 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20494 19886 603 41 0 20453 0
vsize: 81976
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 20283 0 0 0 91944 68 0 0 25 0 1 0 481798713 85393408 20261 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20848 20261 603 41 0 20807 0
vsize: 83392
[startup+930.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 20509 0 0 0 92942 69 0 0 25 0 1 0 481798713 86339584 20487 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21079 20487 603 41 0 21038 0
vsize: 84316
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 20758 0 0 0 93941 70 0 0 25 0 1 0 481798713 87404544 20736 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21339 20736 603 41 0 21298 0
vsize: 85356
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 21051 0 0 0 94940 71 0 0 25 0 1 0 481798713 88600576 21029 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21631 21029 603 41 0 21590 0
vsize: 86524
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 21340 0 0 0 95939 72 0 0 25 0 1 0 481798713 89792512 21318 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21922 21318 603 41 0 21881 0
vsize: 87688
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 21608 0 0 0 96939 73 0 0 25 0 1 0 481798713 90857472 21586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22182 21586 603 41 0 22141 0
vsize: 88728
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 21853 0 0 0 97938 73 0 0 25 0 1 0 481798713 91918336 21831 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22441 21831 603 41 0 22400 0
vsize: 89764
[startup+990.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 22092 0 0 0 98938 74 0 0 25 0 1 0 481798713 92848128 22070 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22668 22070 603 41 0 22627 0
vsize: 90672
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 22314 0 0 0 99937 75 0 0 25 0 1 0 481798713 93777920 22292 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22895 22292 603 41 0 22854 0
vsize: 91580
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 22521 0 0 0 100937 75 0 0 25 0 1 0 481798713 94699520 22499 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23120 22499 603 41 0 23079 0
vsize: 92480
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8578
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 22736 0 0 0 101936 76 0 0 25 0 1 0 481798713 95498240 22714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23315 22714 603 41 0 23274 0
vsize: 93260
[startup+1030.02 s]
Raw data (loadavg): 1.07 0.99 0.92 3/57 8616
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 22950 0 0 0 102930 84 0 0 25 0 1 0 481798713 96428032 22928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23542 22928 603 41 0 23501 0
vsize: 94168
[startup+1040.02 s]
Raw data (loadavg): 1.14 1.00 0.93 2/56 8626
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 23126 0 0 0 103930 84 0 0 25 0 1 0 481798713 97103872 23104 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23707 23104 603 41 0 23666 0
vsize: 94828
[startup+1050.02 s]
Raw data (loadavg): 1.19 1.02 0.93 2/54 8631
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 23357 0 0 0 104929 85 0 0 25 0 1 0 481798713 98566144 23335 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24064 23335 603 41 0 24023 0
vsize: 96256
[startup+1060.02 s]
Raw data (loadavg): 1.16 1.02 0.93 2/54 8631
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 23572 0 0 0 105928 86 0 0 25 0 1 0 481798713 99495936 23550 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24291 23550 603 41 0 24250 0
vsize: 97164
[startup+1070.02 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 8631
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 23764 0 0 0 106927 87 0 0 25 0 1 0 481798713 100294656 23742 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24486 23742 603 41 0 24445 0
vsize: 97944
[startup+1080.02 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 8631
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 23982 0 0 0 107926 88 0 0 25 0 1 0 481798713 101093376 23960 4294967295 134512640 134672761 3221224560 3221223716 134565028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24681 23960 603 41 0 24640 0
vsize: 98724
[startup+1090.02 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 8631
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 24171 0 0 0 108926 89 0 0 25 0 1 0 481798713 101888000 24149 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24875 24149 603 41 0 24834 0
vsize: 99500
[startup+1100.02 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 8631
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 24348 0 0 0 109925 90 0 0 25 0 1 0 481798713 102563840 24326 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25040 24326 603 41 0 24999 0
vsize: 100160
[startup+1110.02 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 8631
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 24528 0 0 0 110924 91 0 0 25 0 1 0 481798713 103415808 24506 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25248 24506 603 41 0 25207 0
vsize: 100992
[startup+1120.02 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 24701 0 0 0 111923 92 0 0 25 0 1 0 481798713 104071168 24679 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25408 24679 603 41 0 25367 0
vsize: 101632
[startup+1130.02 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 24893 0 0 0 112923 92 0 0 25 0 1 0 481798713 104865792 24871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25602 24871 603 41 0 25561 0
vsize: 102408
[startup+1140.02 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 25066 0 0 0 113923 92 0 0 25 0 1 0 481798713 105521152 25044 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25762 25044 603 41 0 25721 0
vsize: 103048
[startup+1150.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 25111 0 0 0 114923 93 0 0 25 0 1 0 481798713 105787392 25089 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25827 25089 603 41 0 25786 0
vsize: 103308
[startup+1160.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 25111 0 0 0 115923 93 0 0 25 0 1 0 481798713 105787392 25089 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25827 25089 603 41 0 25786 0
vsize: 103308
[startup+1170.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 25111 0 0 0 116924 93 0 0 25 0 1 0 481798713 105787392 25089 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25827 25089 603 41 0 25786 0
vsize: 103308
[startup+1180.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 25111 0 0 0 117924 93 0 0 25 0 1 0 481798713 105787392 25089 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25827 25089 603 41 0 25786 0
vsize: 103308
[startup+1190.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 25111 0 0 0 118924 93 0 0 25 0 1 0 481798713 105787392 25089 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25827 25089 603 41 0 25786 0
vsize: 103308
[startup+1200.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 8633
Raw data (stat): 8578 (minisat+) R 8577 3260 3259 0 -1 0 25111 0 0 0 119924 93 0 0 25 0 1 0 481798713 105787392 25089 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25827 25089 603 41 0 25786 0
vsize: 103308
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.01 1.00 0.93 1/54 8633
Raw data (stat): 8578 (minisat+) Z 8577 3260 3259 0 -1 12 25114 0 0 0 119924 97 0 0 25 0 1 0 481798713 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.23
CPU user time (s): 1199.25
CPU system time (s): 0.978851
CPU usage (%): 100.013
Max. virtual memory (Kb): 103308
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####