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 6002

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890624 kB
Buffers:         35340 kB
Cached:          88436 kB
SwapCached:        392 kB
Active:          55924 kB
Inactive:        71104 kB
HighTotal:      131008 kB
HighFree:        38668 kB
LowTotal:       903652 kB
LowFree:        851956 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11360 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:13:08 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4467 7 1200.2 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.85 0.97 0.91 2/54 5218
Raw data (stat): 5218 (runsolver) R 5217 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422922668 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 3605 0 0 0 986 12 0 0 25 0 1 0 422922668 16457728 3583 4294967295 134512640 134672761 3221224560 3221223744 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4018 3583 603 41 0 3977 0
vsize: 16072
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 3692 0 0 0 1986 12 0 0 25 0 1 0 422922668 17055744 3670 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4164 3670 603 41 0 4123 0
vsize: 16656
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 3692 0 0 0 2985 13 0 0 25 0 1 0 422922668 17055744 3670 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4164 3670 603 41 0 4123 0
vsize: 16656
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 3692 0 0 0 3985 13 0 0 25 0 1 0 422922668 17055744 3670 4294967295 134512640 134672761 3221224560 3221223768 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4164 3670 603 41 0 4123 0
vsize: 16656
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 3771 0 0 0 4985 13 0 0 25 0 1 0 422922668 17461248 3749 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3749 603 41 0 4222 0
vsize: 17052
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 4008 0 0 0 5984 14 0 0 25 0 1 0 422922668 18407424 3986 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4494 3986 603 41 0 4453 0
vsize: 17976
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 4389 0 0 0 6983 15 0 0 25 0 1 0 422922668 19931136 4367 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4866 4367 603 41 0 4825 0
vsize: 19464
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 4951 0 0 0 7982 16 0 0 25 0 1 0 422922668 22220800 4929 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4929 603 41 0 5384 0
vsize: 21700
[startup+90.0026 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 5418 0 0 0 8981 17 0 0 25 0 1 0 422922668 24100864 5396 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5884 5396 603 41 0 5843 0
vsize: 23536
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 5910 0 0 0 9980 18 0 0 25 0 1 0 422922668 26238976 5888 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6406 5888 603 41 0 6365 0
vsize: 25624
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 6318 0 0 0 10979 20 0 0 25 0 1 0 422922668 27983872 6296 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6832 6296 603 41 0 6791 0
vsize: 27328
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 6871 0 0 0 11978 21 0 0 25 0 1 0 422922668 30126080 6849 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7355 6849 603 41 0 7314 0
vsize: 29420
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 7352 0 0 0 12976 23 0 0 25 0 1 0 422922668 32129024 7330 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7844 7330 603 41 0 7803 0
vsize: 31376
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 7463 0 0 0 13976 23 0 0 25 0 1 0 422922668 32526336 7441 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7941 7441 603 41 0 7900 0
vsize: 31764
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 7463 0 0 0 14976 23 0 0 25 0 1 0 422922668 32526336 7441 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7941 7441 603 41 0 7900 0
vsize: 31764
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 7463 0 0 0 15976 23 0 0 25 0 1 0 422922668 32526336 7441 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7941 7441 603 41 0 7900 0
vsize: 31764
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 7463 0 0 0 16977 23 0 0 25 0 1 0 422922668 32526336 7441 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7941 7441 603 41 0 7900 0
vsize: 31764
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 7583 0 0 0 17977 23 0 0 25 0 1 0 422922668 33062912 7561 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8072 7561 603 41 0 8031 0
vsize: 32288
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 7970 0 0 0 18976 24 0 0 25 0 1 0 422922668 34676736 7948 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8466 7948 603 41 0 8425 0
vsize: 33864
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 8311 0 0 0 19975 25 0 0 25 0 1 0 422922668 36020224 8289 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8794 8289 603 41 0 8753 0
vsize: 35176
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 8721 0 0 0 20974 27 0 0 25 0 1 0 422922668 37748736 8699 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9216 8699 603 41 0 9175 0
vsize: 36864
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 9235 0 0 0 21972 28 0 0 25 0 1 0 422922668 39751680 9213 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9705 9213 603 41 0 9664 0
vsize: 38820
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 9591 0 0 0 22971 29 0 0 25 0 1 0 422922668 41230336 9569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10066 9569 603 41 0 10025 0
vsize: 40264
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 9984 0 0 0 23971 30 0 0 25 0 1 0 422922668 42835968 9962 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10458 9962 603 41 0 10417 0
vsize: 41832
[startup+250 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 10352 0 0 0 24969 31 0 0 25 0 1 0 422922668 44556288 10330 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10878 10330 603 41 0 10837 0
vsize: 43512
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 10678 0 0 0 25968 33 0 0 25 0 1 0 422922668 45883392 10656 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11202 10656 603 41 0 11161 0
vsize: 44808
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 10995 0 0 0 26967 34 0 0 25 0 1 0 422922668 47235072 10973 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11532 10973 603 41 0 11491 0
vsize: 46128
[startup+279.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 11417 0 0 0 27966 35 0 0 25 0 1 0 422922668 48967680 11395 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11955 11395 603 41 0 11914 0
vsize: 47820
[startup+289.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 11745 0 0 0 28965 37 0 0 25 0 1 0 422922668 50302976 11723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12281 11723 603 41 0 12240 0
vsize: 49124
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 12085 0 0 0 29963 38 0 0 25 0 1 0 422922668 51642368 12063 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12608 12063 603 41 0 12567 0
vsize: 50432
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 12390 0 0 0 30963 39 0 0 25 0 1 0 422922668 52858880 12368 4294967295 134512640 134672761 3221224560 3221223744 134559665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12905 12368 603 41 0 12864 0
vsize: 51620
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 12844 0 0 0 31961 41 0 0 25 0 1 0 422922668 54730752 12822 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13362 12822 603 41 0 13321 0
vsize: 53448
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 13298 0 0 0 32960 42 0 0 25 0 1 0 422922668 56602624 13276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13819 13276 603 41 0 13778 0
vsize: 55276
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 13724 0 0 0 33959 43 0 0 25 0 1 0 422922668 58335232 13702 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14242 13702 603 41 0 14201 0
vsize: 56968
[startup+349.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 14044 0 0 0 34958 44 0 0 25 0 1 0 422922668 59674624 14022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14569 14022 603 41 0 14528 0
vsize: 58276
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 14318 0 0 0 35958 45 0 0 25 0 1 0 422922668 60743680 14296 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14830 14296 603 41 0 14789 0
vsize: 59320
[startup+369.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 14591 0 0 0 36957 45 0 0 25 0 1 0 422922668 61931520 14569 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15120 14569 603 41 0 15079 0
vsize: 60480
[startup+379.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 14860 0 0 0 37956 47 0 0 25 0 1 0 422922668 63000576 14838 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15381 14838 603 41 0 15340 0
vsize: 61524
[startup+389.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 15121 0 0 0 38955 48 0 0 25 0 1 0 422922668 64069632 15099 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15642 15099 603 41 0 15601 0
vsize: 62568
[startup+399.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 15389 0 0 0 39954 49 0 0 25 0 1 0 422922668 65134592 15367 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15902 15367 603 41 0 15861 0
vsize: 63608
[startup+409.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5218
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 15797 0 0 0 40952 51 0 0 25 0 1 0 422922668 66752512 15775 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16297 15775 603 41 0 16256 0
vsize: 65188
[startup+419.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5258
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 16131 0 0 0 41952 52 0 0 25 0 1 0 422922668 68083712 16109 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16622 16109 603 41 0 16581 0
vsize: 66488
[startup+429.999 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 5271
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 16442 0 0 0 42951 53 0 0 25 0 1 0 422922668 69406720 16420 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16945 16420 603 41 0 16904 0
vsize: 67780
[startup+439.999 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 5271
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 16715 0 0 0 43950 54 0 0 25 0 1 0 422922668 70475776 16693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17206 16693 603 41 0 17165 0
vsize: 68824
[startup+449.999 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 5271
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17045 0 0 0 44949 55 0 0 25 0 1 0 422922668 71811072 17023 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17532 17023 603 41 0 17491 0
vsize: 70128
[startup+459.999 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 5271
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 45949 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+469.999 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 5271
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 46949 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+479.999 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 5271
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 47949 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+489.999 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 48949 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+500 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 49950 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+510 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 50950 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+520 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 51950 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+530 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 52950 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+540 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 53950 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+550 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 54950 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+560 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 55951 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+570 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 56951 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+580 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 57951 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+590 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 58951 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+600 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 59951 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+610 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 60951 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+620 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 61951 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+630 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17243 0 0 0 62952 55 0 0 25 0 1 0 422922668 72613888 17221 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17221 603 41 0 17687 0
vsize: 70912
[startup+640 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 63951 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+650.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 64950 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+660 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 65951 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+670 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 66951 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+680.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 67951 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+690 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 68951 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+700 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 69951 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+710 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 70951 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+719.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 71952 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+729.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5273
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 72952 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+739.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 73952 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+750 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 74952 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+760 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 75952 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+770 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 76953 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+780 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17244 0 0 0 77953 56 0 0 25 0 1 0 422922668 72613888 17222 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17222 603 41 0 17687 0
vsize: 70912
[startup+790 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17246 0 0 0 78953 56 0 0 25 0 1 0 422922668 72613888 17224 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17224 603 41 0 17687 0
vsize: 70912
[startup+800 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17248 0 0 0 79953 56 0 0 25 0 1 0 422922668 72613888 17226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17226 603 41 0 17687 0
vsize: 70912
[startup+810 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17250 0 0 0 80953 56 0 0 25 0 1 0 422922668 72613888 17228 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17728 17228 603 41 0 17687 0
vsize: 70912
[startup+820 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17331 0 0 0 81953 57 0 0 25 0 1 0 422922668 73015296 17309 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17826 17309 603 41 0 17785 0
vsize: 71304
[startup+830 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17464 0 0 0 82953 57 0 0 25 0 1 0 422922668 73539584 17442 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17442 603 41 0 17913 0
vsize: 71816
[startup+839.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17591 0 0 0 83952 57 0 0 25 0 1 0 422922668 74067968 17569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18083 17569 603 41 0 18042 0
vsize: 72332
[startup+850 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17713 0 0 0 84952 58 0 0 25 0 1 0 422922668 74592256 17691 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18211 17691 603 41 0 18170 0
vsize: 72844
[startup+860 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 85952 58 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+869.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 86952 58 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223664 134555105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+880 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 87952 58 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+890 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 88952 58 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+900 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 89952 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+910 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 90952 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+920 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 91952 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+930 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 92952 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+940 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 93952 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+950 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 94952 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+959.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 95952 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+969.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 96952 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+979.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 97953 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+989.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 98953 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+999.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 99953 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1010 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 100953 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1020 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 101953 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1030 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 102954 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1040 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 103954 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1050 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 104954 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1060 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 105954 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1070 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 106954 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1080 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 107954 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1090 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 108955 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223664 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1100 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 109955 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1110 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 110955 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1120 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 111955 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1130 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 112955 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1140 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 113955 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1150 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 114956 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1160 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 17840 0 0 0 115956 59 0 0 25 0 1 0 422922668 75124736 17818 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17818 603 41 0 18300 0
vsize: 73364
[startup+1170 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 18059 0 0 0 116955 60 0 0 25 0 1 0 422922668 75923456 18037 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18536 18037 603 41 0 18495 0
vsize: 74144
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 18297 0 0 0 117955 60 0 0 25 0 1 0 422922668 76992512 18275 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18797 18275 603 41 0 18756 0
vsize: 75188
[startup+1190 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 18587 0 0 0 118953 62 0 0 25 0 1 0 422922668 78200832 18565 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19092 18565 603 41 0 19051 0
vsize: 76368
[startup+1200 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5275
Raw data (stat): 5218 (minisat+) R 5217 30701 30700 0 -1 0 18873 0 0 0 119953 63 0 0 25 0 1 0 422922668 79269888 18851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19353 18851 603 41 0 19312 0
vsize: 77412
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 5275
Raw data (stat): 5218 (minisat+) Z 5217 30701 30700 0 -1 12 18876 0 0 0 119953 66 0 0 25 0 1 0 422922668 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.2
CPU user time (s): 1199.53
CPU system time (s): 0.666898
CPU usage (%): 100.014
Max. virtual memory (Kb): 77412
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####