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-3.opb
MD5SUM	b3a3f977e810fc2043ea057a8d94a7d8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-34
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	58245
Number of constraints which are clauses	58245
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 5038

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        866700 kB
Buffers:         31112 kB
Cached:          93348 kB
SwapCached:        524 kB
Active:          44456 kB
Inactive:        83420 kB
HighTotal:      131008 kB
HighFree:        33852 kB
LowTotal:       903652 kB
LowFree:        832848 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34476 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:54:21 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 2975 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58245 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 |   58245   116490 |   19415       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[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 |  103674   223173 |   34558       0        0     nan |  0.000 % |
c |       100 |  103217   222224 |   38013      74      640     8.6 |  0.795 % |
c |       250 |  102277   220190 |   41815     178     1328     7.5 |  2.556 % |
c |       475 |  101299   218072 |   45996     363     3330     9.2 |  4.391 % |
c |       812 |   99047   213116 |   50596     601     6292    10.5 |  8.826 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1154 |   97981   210998 |   32660     842     9717    11.5 |  8.826 % |
c |      1254 |   97456   209833 |   35926     908    10864    12.0 | 12.242 % |
c |      1404 |   96930   208673 |   39518    1038    12408    12.0 | 13.257 % |
c |      1630 |   96171   206966 |   43470    1223    14347    11.7 | 14.977 % |
c |      1967 |   94090   202274 |   47817    1458    16260    11.2 | 18.956 % |
c |      2473 |   92212   198058 |   52599    1787    19115    10.7 | 22.689 % |
c |      3232 |   88553   189636 |   57859    2356    25138    10.7 | 30.105 % |
c |      4372 |   84300   179875 |   63645    3005    31878    10.6 | 38.823 % |
c |      6081 |   80620   171309 |   70009    4307    46466    10.8 | 46.451 % |
c |      8643 |   75017   158019 |   77010    6013    68321    11.4 | 58.474 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9837 |   73511   154433 |   24503    6917    84271    12.2 | 58.474 % |
c |      9937 |   73160   153606 |   26953    6916    84599    12.2 | 62.459 % |
c |     10087 |   73060   153368 |   29648    6999    85824    12.3 | 62.676 % |
c |     10312 |   72828   152824 |   32613    7170    89136    12.4 | 63.163 % |
c |     10649 |   72659   152439 |   35874    7471    94516    12.7 | 63.509 % |
c |     11155 |   72503   152068 |   39462    7865   103845    13.2 | 63.970 % |
c |     11914 |   71669   150067 |   43408    8396   115466    13.8 | 65.675 % |
c |     13055 |   71037   148549 |   47749    9401   141983    15.1 | 67.046 % |
c |     14763 |   70222   146623 |   52524   10862   187323    17.2 | 68.772 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15084 |   70261   146790 |   23420   11142   194649    17.5 | 68.772 % |
c |     15184 |   70145   146515 |   25762   11226   196318    17.5 | 69.049 % |
c |     15334 |   70122   146458 |   28338   11375   199287    17.5 | 69.100 % |
c |     15559 |   70122   146458 |   31172   11600   219368    18.9 | 69.100 % |
c |     15896 |   70114   146440 |   34289   11935   226983    19.0 | 69.116 % |
c |     16402 |   69855   145806 |   37718   12327   241011    19.6 | 69.697 % |
c |     17161 |   69457   144856 |   41489   12860   269839    21.0 | 70.553 % |
c |     18300 |   68230   141868 |   45638   13498   300688    22.3 | 73.307 % |
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 |     19394 |   67923   141108 |   22641   14427   343281    23.8 | 73.307 % |
c |     19495 |   67908   141073 |   24905   14526   347004    23.9 | 74.024 % |
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 |     19613 |   67925   141145 |   22641   14641   351375    24.0 | 74.024 % |
c |     19713 |   67839   140937 |   24905   14731   356033    24.2 | 74.212 % |
c |     19863 |   67762   140750 |   27395   14851   358518    24.1 | 74.384 % |
c |     20088 |   67631   140425 |   30135   14979   363163    24.2 | 74.687 % |
c |     20425 |   67626   140412 |   33148   15243   374131    24.5 | 74.700 % |
c |     20932 |   67626   140412 |   36463   15750   434642    27.6 | 74.700 % |
c |     21692 |   67432   139937 |   40109   16429   458771    27.9 | 75.130 % |
c |     22831 |   67112   139167 |   44120   17411   506808    29.1 | 75.822 % |
c |     24539 |   67069   139072 |   48532   19055   591866    31.1 | 75.899 % |
c |     27101 |   66891   138638 |   53386   21563   774079    35.9 | 76.294 % |
c |     30945 |   66792   138391 |   58724   25311  1005599    39.7 | 76.527 % |
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 |     35844 |   66669   138025 |   22223   30022  1470073    49.0 | 76.527 % |
c |     35945 |   66544   137727 |   24445   30030  1471559    49.0 | 77.089 % |
c |     36097 |   66544   137727 |   26889   30182  1483627    49.2 | 77.089 % |
c |     36322 |   66328   137202 |   29578   30294  1489137    49.2 | 77.568 % |
c |     36659 |   66286   137102 |   32536   30598  1502725    49.1 | 77.657 % |
c |     37165 |   66286   137102 |   35790   31104  1531065    49.2 | 77.657 % |
c |     37924 |   66236   136980 |   39369   31838  1579318    49.6 | 77.772 % |
c |     39063 |   66198   136896 |   43306   32931  1663184    50.5 | 77.845 % |
c |     40771 |   66094   136643 |   47636   34450  1773571    51.5 | 78.081 % |
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 |     43229 |   66119   136738 |   22039   36846  2044619    55.5 | 78.081 % |
c |     43330 |   66082   136649 |   24242   36918  2046357    55.4 | 78.194 % |
c |     43480 |   66082   136649 |   26667   37068  2055234    55.4 | 78.194 % |
c |     43705 |   66061   136598 |   29333   37197  2068198    55.6 | 78.241 % |
c |     44042 |   66061   136598 |   32267   37534  2088672    55.6 | 78.241 % |
c |     44548 |   65988   136417 |   35494   37789  2109858    55.8 | 78.407 % |
c |     45307 |   65967   136364 |   39043   38528  2171262    56.4 | 78.457 % |
c |     46446 |   65967   136364 |   42947   39667  2284055    57.6 | 78.457 % |
c |     48155 |   65911   136232 |   47242   41326  2437988    59.0 | 78.578 % |
c |     50717 |   65911   136232 |   51966   43888  2766324    63.0 | 78.578 % |
c |     54561 |   65908   136225 |   57163   47731  3237086    67.8 | 78.584 % |
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 |     56290 |   65823   135998 |   21941   48563  3297518    67.9 | 78.584 % |
c |     56390 |   65712   135748 |   24135   19988  1396674    69.9 | 78.983 % |
c |     56540 |   65712   135748 |   26548   20138  1404187    69.7 | 78.983 % |
c |     56765 |   65650   135596 |   29203   20338  1414088    69.5 | 79.126 % |
c |     57103 |   65650   135596 |   32123   20676  1442270    69.8 | 79.126 % |
c |     57610 |   65650   135596 |   35336   21183  1470803    69.4 | 79.126 % |
c |     58369 |   65650   135596 |   38869   21942  1512854    68.9 | 79.126 % |
c |     59509 |   65650   135596 |   42756   23082  1617718    70.1 | 79.126 % |
c |     61219 |   65650   135596 |   47032   24792  1814999    73.2 | 79.126 % |
c |     63781 |   65446   135086 |   51735   27327  2124510    77.7 | 79.590 % |
c |     67625 |   65344   134832 |   56909   31081  2420985    77.9 | 79.825 % |
c |     73391 |   65273   134642 |   62600   36808  2997370    81.4 | 80.003 % |
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 |     78259 |   65233   134560 |   21744   41665  3434394    82.4 | 80.003 % |
c |     78359 |   65233   134560 |   23918   41765  3440374    82.4 | 80.114 % |
c |     78509 |   65194   134462 |   26310   41909  3446929    82.2 | 80.209 % |
c |     78735 |   65194   134462 |   28941   42135  3468085    82.3 | 80.209 % |
c |     79072 |   65194   134462 |   31835   42472  3491885    82.2 | 80.209 % |
c |     79578 |   65194   134462 |   35018   42978  3533426    82.2 | 80.209 % |
c |     80337 |   65194   134462 |   38520   43737  3606744    82.5 | 80.209 % |
c |     81476 |   65186   134442 |   42372   44835  3720600    83.0 | 80.228 % |
c |     83184 |   65186   134442 |   46610   46543  3854293    82.8 | 80.228 % |
c |     85747 |   65146   134350 |   51271   49094  4064252    82.8 | 80.307 % |
c |     89591 |   65137   134329 |   56398   52931  4435673    83.8 | 80.326 % |
c |     95358 |   65137   134329 |   62038   58698  5204836    88.7 | 80.326 % |
c |    104009 |   65137   134329 |   68241   67349  6225461    92.4 | 80.326 % |
c |    116985 |   65033   134076 |   75066   80299  7880223    98.1 | 80.561 % |
c |    136446 |   64945   133856 |   82572   99663 10505945   105.4 | 80.761 % |
c |    165638 |   64651   133139 |   90830   37553  3984323   106.1 | 81.418 % |
c |    209427 |   64398   132524 |   99913   81184  8603031   106.0 | 81.986 % |
c |    275112 |   64354   132420 |  109904   41677  3387232    81.3 | 82.081 % |
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 28931
Raw data (stat): 28931 (runsolver) R 28930 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479225511 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 3623 0 0 0 987 11 0 0 25 0 1 0 479225511 16531456 3601 4294967295 134512640 134672761 3221224624 3221223812 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4036 3601 603 41 0 3995 0
vsize: 16144
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 3740 0 0 0 1986 11 0 0 25 0 1 0 479225511 17264640 3718 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4215 3718 603 41 0 4174 0
vsize: 16860
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 3740 0 0 0 2986 11 0 0 25 0 1 0 479225511 17264640 3718 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4215 3718 603 41 0 4174 0
vsize: 16860
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 3740 0 0 0 3986 11 0 0 25 0 1 0 479225511 17264640 3718 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4215 3718 603 41 0 4174 0
vsize: 16860
[startup+50.0014 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 3807 0 0 0 4986 12 0 0 25 0 1 0 479225511 17539072 3785 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4282 3785 603 41 0 4241 0
vsize: 17128
[startup+60.0011 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 4047 0 0 0 5985 12 0 0 25 0 1 0 479225511 18575360 4025 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4535 4025 603 41 0 4494 0
vsize: 18140
[startup+70.001 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 4430 0 0 0 6984 13 0 0 25 0 1 0 479225511 20217856 4408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4936 4408 603 41 0 4895 0
vsize: 19744
[startup+80.0016 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 4998 0 0 0 7981 16 0 0 25 0 1 0 479225511 22511616 4976 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5496 4976 603 41 0 5455 0
vsize: 21984
[startup+90.0013 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 5460 0 0 0 8980 17 0 0 25 0 1 0 479225511 24301568 5438 4294967295 134512640 134672761 3221224624 3221223792 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5933 5438 603 41 0 5892 0
vsize: 23732
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 5970 0 0 0 9979 18 0 0 25 0 1 0 479225511 26574848 5948 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6488 5948 603 41 0 6447 0
vsize: 25952
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 6376 0 0 0 10979 18 0 0 25 0 1 0 479225511 28188672 6354 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6882 6354 603 41 0 6841 0
vsize: 27528
[startup+120.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 6939 0 0 0 11978 19 0 0 25 0 1 0 479225511 30466048 6917 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7438 6917 603 41 0 7397 0
vsize: 29752
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 7435 0 0 0 12976 21 0 0 25 0 1 0 479225511 32473088 7413 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7928 7413 603 41 0 7887 0
vsize: 31712
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 7512 0 0 0 13976 22 0 0 25 0 1 0 479225511 32743424 7490 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7994 7490 603 41 0 7953 0
vsize: 31976
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 7512 0 0 0 14976 22 0 0 25 0 1 0 479225511 32743424 7490 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7994 7490 603 41 0 7953 0
vsize: 31976
[startup+160 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 7512 0 0 0 15976 22 0 0 25 0 1 0 479225511 32743424 7490 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7994 7490 603 41 0 7953 0
vsize: 31976
[startup+170 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 7512 0 0 0 16976 22 0 0 25 0 1 0 479225511 32743424 7490 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7994 7490 603 41 0 7953 0
vsize: 31976
[startup+180 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 7677 0 0 0 17976 22 0 0 25 0 1 0 479225511 33501184 7655 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8179 7655 603 41 0 8138 0
vsize: 32716
[startup+189.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 8054 0 0 0 18975 23 0 0 25 0 1 0 479225511 34975744 8032 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8539 8032 603 41 0 8498 0
vsize: 34156
[startup+199.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 8396 0 0 0 19974 24 0 0 25 0 1 0 479225511 36458496 8374 4294967295 134512640 134672761 3221224624 3221223792 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8374 603 41 0 8860 0
vsize: 35604
[startup+209.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 8871 0 0 0 20972 26 0 0 25 0 1 0 479225511 38309888 8849 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9353 8849 603 41 0 9312 0
vsize: 37412
[startup+219.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 9351 0 0 0 21971 28 0 0 25 0 1 0 479225511 40316928 9329 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9843 9329 603 41 0 9802 0
vsize: 39372
[startup+229.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 9716 0 0 0 22970 29 0 0 25 0 1 0 479225511 41791488 9694 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10203 9694 603 41 0 10162 0
vsize: 40812
[startup+239.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 10103 0 0 0 23969 30 0 0 25 0 1 0 479225511 43384832 10081 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10592 10081 603 41 0 10551 0
vsize: 42368
[startup+249.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 10473 0 0 0 24967 32 0 0 25 0 1 0 479225511 45109248 10451 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11013 10451 603 41 0 10972 0
vsize: 44052
[startup+259.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 10817 0 0 0 25967 33 0 0 25 0 1 0 479225511 46444544 10795 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11339 10795 603 41 0 11298 0
vsize: 45356
[startup+269.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 11135 0 0 0 26966 34 0 0 25 0 1 0 479225511 47788032 11113 4294967295 134512640 134672761 3221224624 3221223760 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11667 11113 603 41 0 11626 0
vsize: 46668
[startup+279.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 11578 0 0 0 27965 35 0 0 25 0 1 0 479225511 49655808 11556 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12123 11556 603 41 0 12082 0
vsize: 48492
[startup+289.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 11894 0 0 0 28964 36 0 0 25 0 1 0 479225511 50864128 11872 4294967295 134512640 134672761 3221224624 3221223728 134559824 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12418 11872 603 41 0 12377 0
vsize: 49672
[startup+299.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 12240 0 0 0 29963 37 0 0 25 0 1 0 479225511 52338688 12218 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12778 12218 603 41 0 12737 0
vsize: 51112
[startup+309.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 12581 0 0 0 30962 38 0 0 25 0 1 0 479225511 53678080 12559 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13105 12559 603 41 0 13064 0
vsize: 52420
[startup+319.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 13043 0 0 0 31961 39 0 0 25 0 1 0 479225511 55554048 13021 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13563 13021 603 41 0 13522 0
vsize: 54252
[startup+329.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 13505 0 0 0 32959 41 0 0 25 0 1 0 479225511 57417728 13483 4294967295 134512640 134672761 3221224624 3221223808 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14018 13484 603 41 0 13977 0
vsize: 56072
[startup+339.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 13881 0 0 0 33959 42 0 0 25 0 1 0 479225511 59027456 13859 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14411 13859 603 41 0 14370 0
vsize: 57644
[startup+349.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 14192 0 0 0 34958 43 0 0 25 0 1 0 479225511 60243968 14170 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14708 14170 603 41 0 14667 0
vsize: 58832
[startup+359.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 14464 0 0 0 35958 43 0 0 25 0 1 0 479225511 61304832 14442 4294967295 134512640 134672761 3221224624 3221223808 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14967 14442 603 41 0 14926 0
vsize: 59868
[startup+369.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 14746 0 0 0 36957 44 0 0 25 0 1 0 479225511 62500864 14724 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14724 603 41 0 15218 0
vsize: 61036
[startup+379.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 15034 0 0 0 37957 45 0 0 25 0 1 0 479225511 63700992 15012 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15552 15012 603 41 0 15511 0
vsize: 62208
[startup+389.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 15269 0 0 0 38956 46 0 0 25 0 1 0 479225511 64647168 15247 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15783 15247 603 41 0 15742 0
vsize: 63132
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 15601 0 0 0 39955 47 0 0 25 0 1 0 479225511 65986560 15579 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16110 15579 603 41 0 16069 0
vsize: 64440
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 16013 0 0 0 40954 48 0 0 25 0 1 0 479225511 67719168 15991 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16533 15991 603 41 0 16492 0
vsize: 66132
[startup+420 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 16314 0 0 0 41954 48 0 0 25 0 1 0 479225511 68919296 16292 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16826 16292 603 41 0 16785 0
vsize: 67304
[startup+430 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 16627 0 0 0 42954 49 0 0 25 0 1 0 479225511 70127616 16605 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17121 16605 603 41 0 17080 0
vsize: 68484
[startup+440 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 16904 0 0 0 43953 50 0 0 25 0 1 0 479225511 71335936 16882 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17416 16882 603 41 0 17375 0
vsize: 69664
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17263 0 0 0 44952 51 0 0 25 0 1 0 479225511 72794112 17241 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17241 603 41 0 17731 0
vsize: 71088
[startup+460 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 45952 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+469.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 46952 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+479.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 47952 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+489.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 48952 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+499.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 49952 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+509.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 50952 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+519.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 51952 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+529.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 52953 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223812 1075347023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+539.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 53953 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223808 134559038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+549.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 54953 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+559.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 55953 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+569.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 56953 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+579.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 57953 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+589.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 58953 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+599.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 59954 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+609.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 60954 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+619.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17280 0 0 0 61954 52 0 0 25 0 1 0 479225511 72794112 17258 4294967295 134512640 134672761 3221224624 3221223760 134560575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17258 603 41 0 17731 0
vsize: 71088
[startup+629.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 62953 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+639.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 63953 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+649.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 64953 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+659.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 65953 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+669.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 66953 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+679.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 67953 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+689.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 68953 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+699.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 69954 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+709.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 70954 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+719.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 71954 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+729.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 72954 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+739.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 73954 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+749.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 74955 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+759.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 75955 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+769.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17281 0 0 0 76955 52 0 0 25 0 1 0 479225511 72794112 17259 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17259 603 41 0 17731 0
vsize: 71088
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17283 0 0 0 77955 52 0 0 25 0 1 0 479225511 72794112 17261 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17261 603 41 0 17731 0
vsize: 71088
[startup+789.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17285 0 0 0 78955 52 0 0 25 0 1 0 479225511 72794112 17263 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17263 603 41 0 17731 0
vsize: 71088
[startup+799.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17287 0 0 0 79956 52 0 0 25 0 1 0 479225511 72794112 17265 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 17265 603 41 0 17731 0
vsize: 71088
[startup+810 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17353 0 0 0 80956 52 0 0 25 0 1 0 479225511 73056256 17331 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17836 17331 603 41 0 17795 0
vsize: 71344
[startup+819.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17491 0 0 0 81955 53 0 0 25 0 1 0 479225511 73588736 17469 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17966 17469 603 41 0 17925 0
vsize: 71864
[startup+829.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17620 0 0 0 82955 53 0 0 25 0 1 0 479225511 74121216 17598 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18096 17598 603 41 0 18055 0
vsize: 72384
[startup+839.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17742 0 0 0 83955 54 0 0 25 0 1 0 479225511 74682368 17720 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18233 17720 603 41 0 18192 0
vsize: 72932
[startup+849.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17873 0 0 0 84955 54 0 0 25 0 1 0 479225511 75206656 17851 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17851 603 41 0 18320 0
vsize: 73444
[startup+859.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 85955 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+869.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 86955 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+879.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 87955 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+889.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 88955 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+899.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 89955 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+910 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 90955 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+920 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 91955 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+930 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 92956 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+940 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 93956 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+950 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 94956 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+960.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 95956 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+970 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 96956 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+980 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 97956 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+990 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 98957 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 99957 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 100957 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1020 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 101957 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1030 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 102957 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1040 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 103958 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1050 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 104958 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1060 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 105958 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1070 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 106958 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1080 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 107958 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1090 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 108959 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1100 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 109959 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1110 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 110959 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1120 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 111959 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1130 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 112959 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1140 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17876 0 0 0 113960 54 0 0 25 0 1 0 479225511 75206656 17854 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17854 603 41 0 18320 0
vsize: 73444
[startup+1150 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 17898 0 0 0 114960 54 0 0 25 0 1 0 479225511 75341824 17876 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18394 17876 603 41 0 18353 0
vsize: 73576
[startup+1160 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 18183 0 0 0 115959 54 0 0 25 0 1 0 479225511 76419072 18161 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18657 18161 603 41 0 18616 0
vsize: 74628
[startup+1170 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 18428 0 0 0 116959 55 0 0 25 0 1 0 479225511 77488128 18406 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18918 18406 603 41 0 18877 0
vsize: 75672
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 18718 0 0 0 117958 57 0 0 25 0 1 0 479225511 78700544 18696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19214 18696 603 41 0 19173 0
vsize: 76856
[startup+1190 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 19006 0 0 0 118957 57 0 0 25 0 1 0 479225511 79896576 18984 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19506 18984 603 41 0 19465 0
vsize: 78024
[startup+1200 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28931
Raw data (stat): 28931 (minisat+) R 28930 26298 26297 0 -1 0 19295 0 0 0 119957 58 0 0 25 0 1 0 479225511 81100800 19273 4294967295 134512640 134672761 3221224624 3221223728 134559829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19800 19273 603 41 0 19759 0
vsize: 79200
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28931
Raw data (stat): 28931 (minisat+) Z 28930 26298 26297 0 -1 12 19298 0 0 0 119957 62 0 0 25 0 1 0 479225511 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.19
CPU user time (s): 1199.57
CPU system time (s): 0.620905
CPU usage (%): 100.012
Max. virtual memory (Kb): 79200
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####