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-4.opb
MD5SUM	2b591d1b24a201f365bc505135aa0578
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.07
Number of variables	945
Total number of constraints	58549
Number of constraints which are clauses	58549
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 5039

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        854440 kB
Buffers:         33696 kB
Cached:         105948 kB
SwapCached:       2476 kB
Active:          52024 kB
Inactive:        93036 kB
HighTotal:      131008 kB
HighFree:        21896 kB
LowTotal:       903652 kB
LowFree:        832544 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29572 kB
Committed_AS:    63604 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:54:25 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 2984 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58549 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 |   58549   117098 |   19516       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -33[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 |  104166   224223 |   34722       0        0     nan |  0.000 % |
c |       100 |  103642   223111 |   38194      76      983    12.9 |  0.946 % |
c |       250 |  103156   222095 |   42013     185     1779     9.6 |  1.795 % |
c |       475 |  102265   220194 |   46214     359     3317     9.2 |  3.414 % |
c |       814 |  101075   217600 |   50836     639     5778     9.0 |  5.664 % |
c |      1320 |   97538   209751 |   55920    1003    12819    12.8 | 12.575 % |
c |      2079 |   93642   200909 |   61512    1463    18801    12.9 | 20.467 % |
c |      3218 |   88661   189630 |   67663    2127    26524    12.5 | 30.497 % |
c |      4927 |   82400   175157 |   74429    3225    35325    11.0 | 43.267 % |
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 |      5415 |   81313   172721 |   27104    3561    38639    10.9 | 43.267 % |
c |      5515 |   81068   172126 |   29814    3614    39218    10.9 | 46.298 % |
c |      5665 |   80657   171144 |   32795    3742    40921    10.9 | 47.176 % |
c |      5890 |   79982   169546 |   36075    3902    43480    11.1 | 48.620 % |
c |      6227 |   79003   167290 |   39682    4118    45635    11.1 | 50.642 % |
c |      6733 |   78063   165079 |   43651    4430    49480    11.2 | 52.651 % |
c |      7493 |   76096   160443 |   48016    4837    55581    11.5 | 56.880 % |
c |      8632 |   74589   156885 |   52818    5773    73298    12.7 | 60.129 % |
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 |      9964 |   72294   151476 |   24098    6717    92845    13.8 | 60.129 % |
c |     10064 |   72294   151476 |   26507    6817    96622    14.2 | 65.090 % |
c |     10214 |   72243   151364 |   29158    6960    98656    14.2 | 65.186 % |
c |     10440 |   72148   151147 |   32074    7150   102420    14.3 | 65.368 % |
c |     10777 |   71910   150582 |   35281    7453   109836    14.7 | 65.878 % |
c |     11283 |   71431   149450 |   38810    7849   116929    14.9 | 66.893 % |
c |     12042 |   70162   146309 |   42691    8318   128370    15.4 | 69.772 % |
c |     13181 |   69233   144085 |   46960    9095   152049    16.7 | 71.811 % |
c |     14889 |   68025   141190 |   51656   10405   194546    18.7 | 74.475 % |
c |     17451 |   67465   139846 |   56821   12599   292482    23.2 | 75.681 % |
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 |     18058 |   67414   139655 |   22471   13154   334103    25.4 | 75.681 % |
c |     18158 |   67414   139655 |   24718   13254   340082    25.7 | 75.807 % |
c |     18309 |   67399   139620 |   27189   13361   344290    25.8 | 75.839 % |
c |     18534 |   66939   138489 |   29908   13378   346429    25.9 | 76.889 % |
c |     18872 |   66842   138270 |   32899   13666   357163    26.1 | 77.077 % |
c |     19378 |   66767   138089 |   36189   14080   377022    26.8 | 77.243 % |
c |     20137 |   66615   137726 |   39808   14759   398503    27.0 | 77.575 % |
c |     21276 |   66398   137195 |   43789   15773   445835    28.3 | 78.060 % |
c |     22984 |   66398   137195 |   48168   17481   625306    35.8 | 78.060 % |
c |     25546 |   66066   136404 |   52985   19769   794427    40.2 | 78.788 % |
c |     29390 |   65853   135895 |   58283   23401  1067190    45.6 | 79.253 % |
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 |     32637 |   65821   135848 |   21940   26636  1446264    54.3 | 79.253 % |
c |     32737 |   65732   135626 |   24134   26685  1448385    54.3 | 79.603 % |
c |     32887 |   65727   135615 |   26547   26818  1455138    54.3 | 79.613 % |
c |     33113 |   65727   135615 |   29202   27044  1474034    54.5 | 79.613 % |
c |     33450 |   65697   135543 |   32122   27355  1497434    54.7 | 79.680 % |
c |     33956 |   65697   135543 |   35334   27861  1538713    55.2 | 79.680 % |
c |     34715 |   65589   135270 |   38868   28521  1585884    55.6 | 79.931 % |
c |     35855 |   65482   135009 |   42754   29577  1655703    56.0 | 80.169 % |
c |     37563 |   65482   135009 |   47030   31285  1797921    57.5 | 80.169 % |
c |     40127 |   65243   134410 |   51733   33432  1984818    59.4 | 80.735 % |
c |     43971 |   64998   133825 |   56906   36983  2317054    62.7 | 81.263 % |
c |     49737 |   64814   133363 |   62597   42396  2877508    67.9 | 81.692 % |
c |     58388 |   64619   132884 |   68857   50672  3796235    74.9 | 82.131 % |
c |     71362 |   64480   132543 |   75742   63342  5261377    83.1 | 82.449 % |
c |     90823 |   64425   132404 |   83317   82608  8035630    97.3 | 82.582 % |
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 |    109905 |   64414   132357 |   21471  101407 10380699   102.4 | 82.582 % |
c |    110006 |   64386   132284 |   23618   21811  1640548    75.2 | 82.679 % |
c |    110156 |   64386   132284 |   25979   21961  1645897    74.9 | 82.679 % |
c |    110381 |   64386   132284 |   28577   22186  1658364    74.7 | 82.679 % |
c |    110718 |   64386   132284 |   31435   22523  1685423    74.8 | 82.679 % |
c |    111224 |   64384   132278 |   34579   23001  1726413    75.1 | 82.685 % |
c |    111983 |   64356   132212 |   38037   23758  1797994    75.7 | 82.745 % |
c |    113124 |   64356   132212 |   41840   24899  1928522    77.5 | 82.745 % |
c |    114832 |   64356   132212 |   46024   26607  2074157    78.0 | 82.745 % |
c |    117394 |   64321   132129 |   50627   29164  2294029    78.7 | 82.822 % |
c |    121238 |   64321   132129 |   55690   33008  2737094    82.9 | 82.822 % |
c |    127004 |   64317   132119 |   61259   38771  3371390    87.0 | 82.831 % |
c |    135653 |   64295   132065 |   67385   47415  4522685    95.4 | 82.882 % |
c |    148627 |   64254   131966 |   74123   60336  6178176   102.4 | 82.974 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    163149 |   64183   131807 |   21394   74787  7692198   102.9 | 82.974 % |
c |    163249 |   64183   131807 |   23533   20074  1358818    67.7 | 83.143 % |
c |    163399 |   64183   131807 |   25886   20224  1366314    67.6 | 83.143 % |
c |    163625 |   64183   131807 |   28475   20450  1379110    67.4 | 83.143 % |
c |    163962 |   64183   131807 |   31322   20787  1392044    67.0 | 83.143 % |
c |    164468 |   64183   131807 |   34455   21293  1434386    67.4 | 83.143 % |
c |    165229 |   64153   131727 |   37900   22051  1483457    67.3 | 83.222 % |
c |    166369 |   64153   131727 |   41690   23191  1600656    69.0 | 83.222 % |
c |    168077 |   64134   131680 |   45859   24890  1783760    71.7 | 83.267 % |
c |    170639 |   64102   131604 |   50445   27431  2021386    73.7 | 83.337 % |
c |    174484 |   64099   131597 |   55490   31274  2339999    74.8 | 83.343 % |
c |    180250 |   64099   131597 |   61039   37040  2928223    79.1 | 83.343 % |
c |    188899 |   64034   131440 |   67143   45638  3846777    84.3 | 83.489 % |
c |    201873 |   63981   131315 |   73857   58555  5634637    96.2 | 83.603 % |
c |    221334 |   63975   131301 |   81243   78014  7981254   102.3 | 83.616 % |
c |    250528 |   63908   131132 |   89368  107123 11438473   106.8 | 83.778 % |
c |    294319 |   63902   131118 |   98304   53229  4759432    89.4 | 83.791 % |
c |    360004 |   63735   130700 |  108135  118856 12406551   104.4 | 84.188 % |
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.84 0.94 0.90 2/54 25886
Raw data (stat): 25886 (runsolver) R 25885 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479232514 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0013 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 3629 0 0 0 988 11 0 0 25 0 1 0 479232514 16568320 3607 4294967295 134512640 134672761 3221224624 3221223796 134556664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4045 3607 603 41 0 4004 0
vsize: 16180
[startup+20.0018 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 3640 0 0 0 1987 11 0 0 25 0 1 0 479232514 16568320 3618 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4045 3618 603 41 0 4004 0
vsize: 16180
[startup+30.0022 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 3648 0 0 0 2987 11 0 0 25 0 1 0 479232514 16568320 3626 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4045 3626 603 41 0 4004 0
vsize: 16180
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 3769 0 0 0 3986 11 0 0 25 0 1 0 479232514 17444864 3747 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4259 3747 603 41 0 4218 0
vsize: 17036
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 3797 0 0 0 4986 11 0 0 25 0 1 0 479232514 17604608 3775 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4298 3775 603 41 0 4257 0
vsize: 17192
[startup+60.0034 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 4056 0 0 0 5985 12 0 0 25 0 1 0 479232514 18534400 4034 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4525 4034 603 41 0 4484 0
vsize: 18100
[startup+70.0045 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 4560 0 0 0 6983 14 0 0 25 0 1 0 479232514 20631552 4538 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5037 4538 603 41 0 4996 0
vsize: 20148
[startup+80.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 5176 0 0 0 7981 16 0 0 25 0 1 0 479232514 23183360 5154 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5660 5154 603 41 0 5619 0
vsize: 22640
[startup+90.0053 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 5643 0 0 0 8980 18 0 0 25 0 1 0 479232514 25092096 5621 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6126 5621 603 41 0 6085 0
vsize: 24504
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 6034 0 0 0 9979 19 0 0 25 0 1 0 479232514 26832896 6012 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6551 6012 603 41 0 6510 0
vsize: 26204
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 6534 0 0 0 10978 20 0 0 25 0 1 0 479232514 28852224 6512 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7044 6512 603 41 0 7003 0
vsize: 28176
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 7059 0 0 0 11976 22 0 0 25 0 1 0 479232514 31002624 7037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7569 7037 603 41 0 7528 0
vsize: 30276
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 7506 0 0 0 12975 24 0 0 25 0 1 0 479232514 32747520 7484 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7995 7484 603 41 0 7954 0
vsize: 31980
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 7954 0 0 0 13973 25 0 0 25 0 1 0 479232514 34635776 7932 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8456 7932 603 41 0 8415 0
vsize: 33824
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 8412 0 0 0 14972 26 0 0 25 0 1 0 479232514 36499456 8390 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8911 8390 603 41 0 8870 0
vsize: 35644
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 8836 0 0 0 15971 27 0 0 25 0 1 0 479232514 38113280 8814 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9305 8814 603 41 0 9264 0
vsize: 37220
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 9295 0 0 0 16971 28 0 0 25 0 1 0 479232514 39989248 9273 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9763 9273 603 41 0 9722 0
vsize: 39052
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 9695 0 0 0 17969 29 0 0 25 0 1 0 479232514 41725952 9673 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9673 603 41 0 10146 0
vsize: 40748
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 10101 0 0 0 18968 31 0 0 25 0 1 0 479232514 43589632 10079 4294967295 134512640 134672761 3221224624 3221223728 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10642 10079 603 41 0 10601 0
vsize: 42568
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 10518 0 0 0 19967 32 0 0 25 0 1 0 479232514 45322240 10496 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11065 10496 603 41 0 11024 0
vsize: 44260
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 10923 0 0 0 20967 33 0 0 25 0 1 0 479232514 46927872 10901 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11457 10901 603 41 0 11416 0
vsize: 45828
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 11318 0 0 0 21966 34 0 0 25 0 1 0 479232514 48521216 11296 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11846 11296 603 41 0 11805 0
vsize: 47384
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 11679 0 0 0 22965 35 0 0 25 0 1 0 479232514 49983488 11657 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11657 603 41 0 12162 0
vsize: 48812
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 12025 0 0 0 23964 36 0 0 25 0 1 0 479232514 51462144 12003 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12564 12003 603 41 0 12523 0
vsize: 50256
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 12394 0 0 0 24964 36 0 0 25 0 1 0 479232514 52928512 12372 4294967295 134512640 134672761 3221224624 3221223808 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12922 12372 603 41 0 12881 0
vsize: 51688
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 12791 0 0 0 25962 38 0 0 25 0 1 0 479232514 54546432 12769 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13317 12769 603 41 0 13276 0
vsize: 53268
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 13152 0 0 0 26962 39 0 0 25 0 1 0 479232514 56025088 13130 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13678 13130 603 41 0 13637 0
vsize: 54712
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 13532 0 0 0 27960 41 0 0 25 0 1 0 479232514 57495552 13510 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14037 13510 603 41 0 13996 0
vsize: 56148
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 13880 0 0 0 28960 41 0 0 25 0 1 0 479232514 58957824 13858 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14394 13858 603 41 0 14353 0
vsize: 57576
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 14188 0 0 0 29959 42 0 0 25 0 1 0 479232514 60153856 14166 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14686 14166 603 41 0 14645 0
vsize: 58744
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 14505 0 0 0 30958 43 0 0 25 0 1 0 479232514 61493248 14483 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15013 14483 603 41 0 14972 0
vsize: 60052
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 14816 0 0 0 31958 44 0 0 25 0 1 0 479232514 62836736 14794 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15341 14794 603 41 0 15300 0
vsize: 61364
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 32957 44 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 33957 44 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 34957 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 35958 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 36957 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 37958 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 38958 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 39958 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 40958 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 41958 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 42958 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 43958 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 44959 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 45959 45 0 0 25 0 1 0 479232514 63557632 14996 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15517 14996 603 41 0 15476 0
vsize: 62068
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 46959 45 0 0 25 0 1 0 479232514 63549440 14996 4294967295 134512640 134672761 3221224624 3221223620 1075351190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15515 14996 603 41 0 15474 0
vsize: 62060
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 47959 45 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 48959 45 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 49959 45 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 50960 45 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 51960 45 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 52960 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 53960 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 54960 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 55960 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 56960 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 57960 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 58961 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 59961 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 60961 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 61961 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 62961 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 63961 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 64962 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 65962 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 66962 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15018 0 0 0 67962 46 0 0 25 0 1 0 479232514 63541248 14996 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14996 603 41 0 15472 0
vsize: 62052
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15019 0 0 0 68962 46 0 0 25 0 1 0 479232514 63541248 14997 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14997 603 41 0 15472 0
vsize: 62052
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15326 0 0 0 69962 47 0 0 25 0 1 0 479232514 64876544 15304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15839 15304 603 41 0 15798 0
vsize: 63356
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15614 0 0 0 70961 47 0 0 25 0 1 0 479232514 66072576 15592 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16131 15592 603 41 0 16090 0
vsize: 64524
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 15900 0 0 0 71961 48 0 0 25 0 1 0 479232514 67268608 15878 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16423 15878 603 41 0 16382 0
vsize: 65692
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 16183 0 0 0 72961 49 0 0 25 0 1 0 479232514 68337664 16161 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16684 16161 603 41 0 16643 0
vsize: 66736
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 16473 0 0 0 73960 49 0 0 25 0 1 0 479232514 69550080 16451 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16980 16451 603 41 0 16939 0
vsize: 67920
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 16718 0 0 0 74959 50 0 0 25 0 1 0 479232514 70483968 16696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17208 16696 603 41 0 17167 0
vsize: 68832
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 16960 0 0 0 75959 50 0 0 25 0 1 0 479232514 71544832 16938 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17467 16938 603 41 0 17426 0
vsize: 69868
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17162 0 0 0 76959 51 0 0 25 0 1 0 479232514 72339456 17140 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17661 17140 603 41 0 17620 0
vsize: 70644
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17354 0 0 0 77958 51 0 0 25 0 1 0 479232514 73134080 17332 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17855 17332 603 41 0 17814 0
vsize: 71420
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17513 0 0 0 78957 52 0 0 25 0 1 0 479232514 73797632 17491 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18017 17491 603 41 0 17976 0
vsize: 72068
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 79957 52 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 80958 52 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223760 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 81958 52 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 82958 52 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 83958 52 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 84958 52 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 85958 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 86958 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 87958 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 88958 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+900.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 89958 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+910.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 90958 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223748 134566054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+920.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 91959 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+930.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 92959 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+940.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 93959 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 94959 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223760 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 95959 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 96959 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 97960 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 98960 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 99960 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223808 134559356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 100960 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 101960 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 102960 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 103960 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 104961 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17555 0 0 0 105961 53 0 0 25 0 1 0 479232514 73932800 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17533 603 41 0 18009 0
vsize: 72200
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17556 0 0 0 106961 53 0 0 25 0 1 0 479232514 73932800 17534 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17534 603 41 0 18009 0
vsize: 72200
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17556 0 0 0 107961 53 0 0 25 0 1 0 479232514 73932800 17534 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17534 603 41 0 18009 0
vsize: 72200
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17556 0 0 0 108961 53 0 0 25 0 1 0 479232514 73932800 17534 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18050 17534 603 41 0 18009 0
vsize: 72200
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 17711 0 0 0 109960 54 0 0 25 0 1 0 479232514 74604544 17689 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18214 17689 603 41 0 18173 0
vsize: 72856
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 18008 0 0 0 110959 55 0 0 25 0 1 0 479232514 75812864 17986 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18509 17986 603 41 0 18468 0
vsize: 74036
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 18302 0 0 0 111958 56 0 0 25 0 1 0 479232514 77012992 18280 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18802 18280 603 41 0 18761 0
vsize: 75208
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 18577 0 0 0 112957 57 0 0 25 0 1 0 479232514 78077952 18555 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19062 18555 603 41 0 19021 0
vsize: 76248
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 18795 0 0 0 113956 58 0 0 25 0 1 0 479232514 79048704 18773 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19299 18773 603 41 0 19258 0
vsize: 77196
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 19054 0 0 0 114956 59 0 0 25 0 1 0 479232514 80121856 19032 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19561 19032 603 41 0 19520 0
vsize: 78244
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 19289 0 0 0 115955 60 0 0 25 0 1 0 479232514 81575936 19267 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19916 19267 603 41 0 19875 0
vsize: 79664
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 19548 0 0 0 116955 60 0 0 25 0 1 0 479232514 82649088 19526 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20178 19526 603 41 0 20137 0
vsize: 80712
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 19802 0 0 0 117954 62 0 0 25 0 1 0 479232514 83714048 19780 4294967295 134512640 134672761 3221224624 3221223728 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20438 19780 603 41 0 20397 0
vsize: 81752
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 19802 0 0 0 118954 62 0 0 25 0 1 0 479232514 83714048 19780 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20438 19780 603 41 0 20397 0
vsize: 81752
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25886
Raw data (stat): 25886 (minisat+) R 25885 22612 22611 0 -1 0 19802 0 0 0 119954 62 0 0 25 0 1 0 479232514 83714048 19780 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20438 19780 603 41 0 20397 0
vsize: 81752
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25886
Raw data (stat): 25886 (minisat+) Z 25885 22612 22611 0 -1 12 19805 0 0 0 119954 66 0 0 25 0 1 0 479232514 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.05
CPU time (s): 1200.21
CPU user time (s): 1199.55
CPU system time (s): 0.662899
CPU usage (%): 100.013
Max. virtual memory (Kb): 81752
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####