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-5.opb
MD5SUM	7850e0b228f4ef5ee038a9c3595683ab
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-33
Optimality of the best value was proved	NO
Number of terms in the objective function	945
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	945
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	945
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	945
Total number of constraints	58579
Number of constraints which are clauses	58579
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 6378

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 04:44:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4845 boxname=wulflinc2 idbench=333 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7850e0b228f4ef5ee038a9c3595683ab  /oldhome/oroussel/tmp/wulflinc2/normalized-frb45-21-5.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-frb45-21-5.opb /oldhome/oroussel/tmp/wulflinc2/normalized-frb45-21-5.opb
IDLAUNCH: 4845
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        887512 kB
Buffers:         35656 kB
Cached:          90480 kB
SwapCached:          4 kB
Active:          59684 kB
Inactive:        69348 kB
HighTotal:      131008 kB
HighFree:        36652 kB
LowTotal:       903652 kB
LowFree:        850860 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12552 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:04:56 (client local time) WITH STATUS 10 IN 1200.76 SECONDS
stats: 4845 7 1200.76 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58579 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 |   58579   117158 |   19526       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  150325   331906 |   50108       0        0     nan |  0.000 % |
c |       101 |  150325   331906 |   55118     101      811     8.0 |  0.004 % |
c |       251 |  148966   328805 |   60630     205     1319     6.4 |  1.292 % |
c |       476 |  146491   323138 |   66693     370     2193     5.9 |  3.683 % |
c |       813 |  143928   317307 |   73363     652     4417     6.8 |  6.061 % |
c |      1319 |  140158   308658 |   80699    1060    13483    12.7 |  9.764 % |
c |      2078 |  134153   294847 |   88769    1623    18437    11.4 | 15.745 % |
c |      3217 |  124277   272007 |   97646    2461    26724    10.9 | 25.798 % |
c |      4927 |  112216   243915 |  107410    3628    39249    10.8 | 38.401 % |
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 |      6111 |  104143   225226 |   34714    4335    47041    10.9 | 38.401 % |
c |      6212 |  103786   224404 |   38185    4407    47434    10.8 | 47.502 % |
c |      6362 |  102819   222123 |   42003    4505    49096    10.9 | 48.544 % |
c |      6588 |  101174   218266 |   46204    4577    50166    11.0 | 50.320 % |
c |      6927 |   98105   211076 |   50824    4651    52201    11.2 | 53.629 % |
c |      7433 |   95085   203994 |   55907    4886    53927    11.0 | 56.887 % |
c |      8192 |   90657   193600 |   61497    5232    58051    11.1 | 61.745 % |
c |      9331 |   85276   180992 |   67647    5708    64701    11.3 | 67.657 % |
c |     11039 |   80584   169953 |   74412    6735    78399    11.6 | 72.825 % |
c |     13601 |   75523   158031 |   81853    8036   103307    12.9 | 78.539 % |
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 |     15310 |   73436   153106 |   24478    8891   139518    15.7 | 78.539 % |
c |     15410 |   73412   153051 |   26925    8960   140704    15.7 | 80.843 % |
c |     15560 |   73337   152875 |   29618    9077   142513    15.7 | 80.929 % |
c |     15785 |   73012   152108 |   32580    9186   148806    16.2 | 81.290 % |
c |     16123 |   72674   151307 |   35838    9311   152822    16.4 | 81.686 % |
c |     16629 |   72412   150692 |   39422    9605   162242    16.9 | 81.983 % |
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 |     17102 |   71984   149703 |   23994    9804   172723    17.6 | 81.983 % |
c |     17202 |   71984   149703 |   26393    9904   174543    17.6 | 82.476 % |
c |     17353 |   71730   149107 |   29032    9910   176118    17.8 | 82.760 % |
c |     17578 |   71423   148376 |   31936    9918   175534    17.7 | 83.127 % |
c |     17915 |   71270   148013 |   35129   10172   183406    18.0 | 83.309 % |
c |     18421 |   71171   147782 |   38642   10641   197826    18.6 | 83.417 % |
c |     19182 |   71151   147736 |   42506   11363   248192    21.8 | 83.437 % |
c |     20321 |   70619   146483 |   46757   12121   276090    22.8 | 84.052 % |
c |     22030 |   70201   145499 |   51433   13538   329070    24.3 | 84.515 % |
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 |     24587 |   69650   144175 |   23216   15392   445716    29.0 | 84.515 % |
c |     24687 |   69650   144175 |   25537   15492   447610    28.9 | 85.122 % |
c |     24838 |   69650   144175 |   28091   15643   450470    28.8 | 85.122 % |
c |     25063 |   69650   144175 |   30900   15868   457223    28.8 | 85.122 % |
c |     25400 |   69628   144122 |   33990   16137   465455    28.8 | 85.151 % |
c |     25906 |   69628   144122 |   37389   16643   489358    29.4 | 85.151 % |
c |     26665 |   69333   143428 |   41128   16629   516312    31.0 | 85.496 % |
c |     27804 |   69333   143428 |   45241   17768   634833    35.7 | 85.496 % |
c |     29513 |   69221   143170 |   49765   19369   792464    40.9 | 85.610 % |
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 |     32053 |   69273   143300 |   23091   21909  1012590    46.2 | 85.610 % |
c |     32153 |   69273   143300 |   25400   22009  1016657    46.2 | 85.616 % |
c |     32303 |   69273   143300 |   27940   22159  1023041    46.2 | 85.616 % |
c |     32528 |   69187   143099 |   30734   22225  1025959    46.2 | 85.708 % |
c |     32866 |   69187   143099 |   33807   22563  1044404    46.3 | 85.708 % |
c |     33372 |   69187   143099 |   37188   23069  1063824    46.1 | 85.708 % |
c |     34131 |   69187   143099 |   40907   23828  1118420    46.9 | 85.708 % |
c |     35270 |   69187   143099 |   44997   24967  1192598    47.8 | 85.708 % |
c |     36978 |   69187   143099 |   49497   26675  1359377    51.0 | 85.708 % |
c |     39540 |   69181   143085 |   54447   29236  1647495    56.4 | 85.714 % |
c |     43384 |   69167   143052 |   59892   33058  2009973    60.8 | 85.730 % |
c |     49151 |   69167   143052 |   65881   38825  2460870    63.4 | 85.730 % |
c |     57800 |   68961   142568 |   72469   47072  3196897    67.9 | 85.965 % |
c |     70777 |   68955   142554 |   79716   60044  5395883    89.9 | 85.972 % |
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 |     90095 |   68797   142173 |   22932   79148  7630767    96.4 | 85.972 % |
c |     90196 |   68797   142173 |   25225   19831  1466454    73.9 | 86.148 % |
c |     90347 |   68797   142173 |   27747   19982  1471813    73.7 | 86.147 % |
c |     90572 |   68797   142173 |   30522   20207  1494322    74.0 | 86.147 % |
c |     90909 |   68797   142173 |   33574   20544  1520308    74.0 | 86.148 % |
c |     91415 |   68797   142173 |   36932   21050  1554935    73.9 | 86.147 % |
c |     92175 |   68522   141485 |   40625   21665  1598810    73.8 | 86.462 % |
c |     93314 |   68522   141485 |   44687   22804  1660880    72.8 | 86.462 % |
c |     95023 |   68348   141077 |   49156   24464  1796865    73.4 | 86.662 % |
c |     97585 |   68275   140901 |   54072   27011  1964469    72.7 | 86.739 % |
c |    101429 |   68275   140901 |   59479   30855  2412435    78.2 | 86.739 % |
c |    107196 |   68275   140901 |   65427   36622  2976267    81.3 | 86.739 % |
c |    115845 |   68271   140892 |   71970   45259  3871793    85.5 | 86.742 % |
c |    128819 |   68271   140892 |   79167   58233  5442617    93.5 | 86.742 % |
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 |    146628 |   68258   140863 |   22752   76040  7487448    98.5 | 86.742 % |
c |    146728 |   68258   140863 |   25027   17635  1560362    88.5 | 86.780 % |
c |    146878 |   68190   140701 |   27529   17781  1566136    88.1 | 86.866 % |
c |    147103 |   68190   140701 |   30282   18006  1572695    87.3 | 86.866 % |
c |    147440 |   68178   140673 |   33311   18342  1596333    87.0 | 86.878 % |
c |    147947 |   68178   140673 |   36642   18849  1629629    86.5 | 86.878 % |
c |    148706 |   68178   140673 |   40306   19608  1667557    85.0 | 86.878 % |
c |    149846 |   68178   140673 |   44337   20748  1745400    84.1 | 86.878 % |
c |    151554 |   68178   140673 |   48770   22456  1855038    82.6 | 86.878 % |
c |    154117 |   68178   140673 |   53648   25019  2073989    82.9 | 86.878 % |
c |    157961 |   68174   140664 |   59012   28862  2367867    82.0 | 86.882 % |
c |    163727 |   68174   140664 |   64914   34628  2937796    84.8 | 86.882 % |
c |    172376 |   68164   140641 |   71405   43274  3759322    86.9 | 86.891 % |
c |    185350 |   68160   140632 |   78546   56247  5079126    90.3 | 86.894 % |
c |    204811 |   67972   140182 |   86400   75281  7086638    94.1 | 87.132 % |
c |    234003 |   67898   140009 |   95040  104287  9924469    95.2 | 87.212 % |
c |    277793 |   67888   139986 |  104544   44744  3463513    77.4 | 87.221 % |
c |    343477 |   67858   139915 |  114999  110415 10051832    91.0 | 87.256 % |
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 -C#### 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.94 0.93 2/54 26753
Raw data (stat): 26753 (runsolver) R 26752 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423591671 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.88 0.94 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 3833 0 0 0 987 11 0 0 25 0 1 0 423591671 17764352 3811 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4337 3811 603 41 0 4296 0
vsize: 17348
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.94 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 3841 0 0 0 1986 11 0 0 25 0 1 0 423591671 17764352 3819 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4337 3819 603 41 0 4296 0
vsize: 17348
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.94 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 3844 0 0 0 2987 11 0 0 25 0 1 0 423591671 17764352 3822 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4337 3822 603 41 0 4296 0
vsize: 17348
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.94 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 3967 0 0 0 3985 12 0 0 25 0 1 0 423591671 18612224 3945 4294967295 134512640 134672761 3221224560 3221223732 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4544 3945 603 41 0 4503 0
vsize: 18176
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 3969 0 0 0 4985 12 0 0 25 0 1 0 423591671 18612224 3947 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4544 3947 603 41 0 4503 0
vsize: 18176
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 4009 0 0 0 5985 13 0 0 25 0 1 0 423591671 18681856 3987 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4561 3987 603 41 0 4520 0
vsize: 18244
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 4353 0 0 0 6983 14 0 0 25 0 1 0 423591671 20094976 4331 4294967295 134512640 134672761 3221224560 3221223724 134565030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4331 603 41 0 4865 0
vsize: 19624
[startup+80.0027 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 4990 0 0 0 7982 15 0 0 25 0 1 0 423591671 22712320 4968 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5545 4968 603 41 0 5504 0
vsize: 22180
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 5655 0 0 0 8980 17 0 0 25 0 1 0 423591671 25407488 5633 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6203 5633 603 41 0 6162 0
vsize: 24812
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 6242 0 0 0 9979 19 0 0 25 0 1 0 423591671 27951104 6220 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6824 6220 603 41 0 6783 0
vsize: 27296
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 6691 0 0 0 10978 20 0 0 25 0 1 0 423591671 29835264 6669 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7284 6669 603 41 0 7243 0
vsize: 29136
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 7161 0 0 0 11976 21 0 0 25 0 1 0 423591671 31711232 7139 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 7139 603 41 0 7701 0
vsize: 30968
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 7649 0 0 0 12975 23 0 0 25 0 1 0 423591671 33722368 7627 4294967295 134512640 134672761 3221224560 3221223744 134558836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8233 7627 603 41 0 8192 0
vsize: 32932
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 8274 0 0 0 13973 25 0 0 25 0 1 0 423591671 36257792 8252 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8852 8252 603 41 0 8811 0
vsize: 35408
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 8858 0 0 0 14972 26 0 0 25 0 1 0 423591671 38641664 8836 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9434 8836 603 41 0 9393 0
vsize: 37736
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 9432 0 0 0 15971 27 0 0 25 0 1 0 423591671 40923136 9410 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9991 9410 603 41 0 9950 0
vsize: 39964
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.93 3/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 9910 0 0 0 16970 29 0 0 25 0 1 0 423591671 42930176 9888 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10481 9888 603 41 0 10440 0
vsize: 41924
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 10381 0 0 0 17969 30 0 0 25 0 1 0 423591671 45072384 10359 4294967295 134512640 134672761 3221224560 3221223576 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11004 10359 603 41 0 10963 0
vsize: 44016
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 10727 0 0 0 18967 32 0 0 25 0 1 0 423591671 46538752 10705 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11362 10705 603 41 0 11321 0
vsize: 45448
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 11110 0 0 0 19966 33 0 0 25 0 1 0 423591671 48017408 11088 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11723 11088 603 41 0 11682 0
vsize: 46892
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 11519 0 0 0 20965 34 0 0 25 0 1 0 423591671 49745920 11497 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12145 11497 603 41 0 12104 0
vsize: 48580
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 11900 0 0 0 21964 36 0 0 25 0 1 0 423591671 51212288 11878 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12503 11878 603 41 0 12462 0
vsize: 50012
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 22964 36 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 23964 36 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223696 134560575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 24964 36 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 25963 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 26962 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 27962 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 28962 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 29962 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223664 134555228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 30962 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 31963 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 32963 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 33963 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 34963 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12060 0 0 0 35963 37 0 0 25 0 1 0 423591671 51859456 12038 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 12038 603 41 0 12620 0
vsize: 50644
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 36963 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223664 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 37964 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 38964 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 39964 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 40964 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 41964 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 42964 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 43965 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 44965 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 45965 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 46965 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 47965 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 48966 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12108 0 0 0 49966 37 0 0 25 0 1 0 423591671 52056064 12086 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 12086 603 41 0 12668 0
vsize: 50836
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12312 0 0 0 50965 38 0 0 25 0 1 0 423591671 52994048 12290 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12938 12290 603 41 0 12897 0
vsize: 51752
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12652 0 0 0 51965 39 0 0 25 0 1 0 423591671 54333440 12630 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13265 12630 603 41 0 13224 0
vsize: 53060
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 12977 0 0 0 52964 39 0 0 25 0 1 0 423591671 55668736 12955 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13591 12955 603 41 0 13550 0
vsize: 54364
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 13275 0 0 0 53963 40 0 0 25 0 1 0 423591671 56860672 13253 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13882 13253 603 41 0 13841 0
vsize: 55528
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 13547 0 0 0 54963 41 0 0 25 0 1 0 423591671 57921536 13525 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14141 13525 603 41 0 14100 0
vsize: 56564
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 13769 0 0 0 55962 42 0 0 25 0 1 0 423591671 58851328 13747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14368 13747 603 41 0 14327 0
vsize: 57472
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 14029 0 0 0 56961 43 0 0 25 0 1 0 423591671 59920384 14007 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14629 14007 603 41 0 14588 0
vsize: 58516
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 14285 0 0 0 57961 43 0 0 25 0 1 0 423591671 61005824 14263 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14894 14263 603 41 0 14853 0
vsize: 59576
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 14549 0 0 0 58961 44 0 0 25 0 1 0 423591671 62091264 14527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15159 14527 603 41 0 15118 0
vsize: 60636
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 14804 0 0 0 59960 45 0 0 25 0 1 0 423591671 63041536 14782 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15391 14782 603 41 0 15350 0
vsize: 61564
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 15064 0 0 0 60960 45 0 0 25 0 1 0 423591671 64106496 15042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15651 15042 603 41 0 15610 0
vsize: 62604
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 15301 0 0 0 61960 46 0 0 25 0 1 0 423591671 65040384 15279 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15879 15279 603 41 0 15838 0
vsize: 63516
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 15506 0 0 0 62959 46 0 0 25 0 1 0 423591671 65957888 15484 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16103 15484 603 41 0 16062 0
vsize: 64412
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 15724 0 0 0 63959 47 0 0 25 0 1 0 423591671 66768896 15702 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16301 15702 603 41 0 16260 0
vsize: 65204
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 15930 0 0 0 64958 48 0 0 25 0 1 0 423591671 67571712 15908 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16497 15908 603 41 0 16456 0
vsize: 65988
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16154 0 0 0 65957 48 0 0 25 0 1 0 423591671 68509696 16132 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16726 16132 603 41 0 16685 0
vsize: 66904
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16416 0 0 0 66957 49 0 0 25 0 1 0 423591671 69574656 16394 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16986 16394 603 41 0 16945 0
vsize: 67944
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16670 0 0 0 67957 50 0 0 25 0 1 0 423591671 70643712 16648 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17247 16648 603 41 0 17206 0
vsize: 68988
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 68957 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 69957 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 70957 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 71957 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 72958 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 73957 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223664 134559784 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 74957 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 75957 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 76958 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 77958 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 78958 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 79958 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 80958 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 81959 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 82959 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 83959 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 84959 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 85959 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 86959 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 87960 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 88960 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16705 0 0 0 89960 50 0 0 25 0 1 0 423591671 70774784 16683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16683 603 41 0 17238 0
vsize: 69116
[startup+910.011 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 26753
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16706 0 0 0 90960 50 0 0 25 0 1 0 423591671 70774784 16684 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16684 603 41 0 17238 0
vsize: 69116
[startup+920.251 s]
Raw data (loadavg): 1.29 1.04 0.95 2/57 26794
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16706 0 0 0 91983 50 0 0 25 0 1 0 423591671 70774784 16684 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16684 603 41 0 17238 0
vsize: 69116
[startup+930.586 s]
Raw data (loadavg): 1.24 1.03 0.95 2/54 26806
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16706 0 0 0 93017 50 0 0 25 0 1 0 423591671 70774784 16684 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16684 603 41 0 17238 0
vsize: 69116
[startup+940.585 s]
Raw data (loadavg): 1.21 1.03 0.95 2/54 26806
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16707 0 0 0 94017 50 0 0 25 0 1 0 423591671 70774784 16685 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16685 603 41 0 17238 0
vsize: 69116
[startup+950.585 s]
Raw data (loadavg): 1.17 1.03 0.95 2/54 26806
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16707 0 0 0 95017 50 0 0 25 0 1 0 423591671 70774784 16685 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17279 16685 603 41 0 17238 0
vsize: 69116
[startup+960.586 s]
Raw data (loadavg): 1.15 1.03 0.95 2/54 26806
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16707 0 0 0 96016 51 0 0 25 0 1 0 423591671 70774784 16685 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16685 603 41 0 17238 0
vsize: 69116
[startup+970.586 s]
Raw data (loadavg): 1.12 1.03 0.95 2/54 26806
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16707 0 0 0 97016 51 0 0 25 0 1 0 423591671 70774784 16685 4294967295 134512640 134672761 3221224560 3221223664 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16685 603 41 0 17238 0
vsize: 69116
[startup+980.586 s]
Raw data (loadavg): 1.10 1.03 0.95 2/54 26806
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16707 0 0 0 98016 51 0 0 25 0 1 0 423591671 70774784 16685 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16685 603 41 0 17238 0
vsize: 69116
[startup+990.586 s]
Raw data (loadavg): 1.09 1.03 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16707 0 0 0 99016 51 0 0 25 0 1 0 423591671 70774784 16685 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16685 603 41 0 17238 0
vsize: 69116
[startup+1000.59 s]
Raw data (loadavg): 1.07 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16707 0 0 0 100017 51 0 0 25 0 1 0 423591671 70774784 16685 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16685 603 41 0 17238 0
vsize: 69116
[startup+1010.59 s]
Raw data (loadavg): 1.06 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16707 0 0 0 101017 51 0 0 25 0 1 0 423591671 70774784 16685 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16685 603 41 0 17238 0
vsize: 69116
[startup+1020.59 s]
Raw data (loadavg): 1.05 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16710 0 0 0 102017 51 0 0 25 0 1 0 423591671 70774784 16688 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17279 16688 603 41 0 17238 0
vsize: 69116
[startup+1030.59 s]
Raw data (loadavg): 1.12 1.04 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 16863 0 0 0 103017 51 0 0 25 0 1 0 423591671 71434240 16841 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17440 16841 603 41 0 17399 0
vsize: 69760
[startup+1040.59 s]
Raw data (loadavg): 1.10 1.04 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 17028 0 0 0 104016 52 0 0 25 0 1 0 423591671 72613888 17006 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17728 17006 603 41 0 17687 0
vsize: 70912
[startup+1050.59 s]
Raw data (loadavg): 1.09 1.03 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 17183 0 0 0 105016 52 0 0 25 0 1 0 423591671 73269248 17161 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17888 17161 603 41 0 17847 0
vsize: 71552
[startup+1060.59 s]
Raw data (loadavg): 1.07 1.03 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 17346 0 0 0 106016 53 0 0 25 0 1 0 423591671 73928704 17324 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18049 17324 603 41 0 18008 0
vsize: 72196
[startup+1070.59 s]
Raw data (loadavg): 1.06 1.03 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 17483 0 0 0 107016 53 0 0 25 0 1 0 423591671 74457088 17461 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18178 17461 603 41 0 18137 0
vsize: 72712
[startup+1080.59 s]
Raw data (loadavg): 1.05 1.03 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 17640 0 0 0 108015 54 0 0 25 0 1 0 423591671 75116544 17618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18339 17618 603 41 0 18298 0
vsize: 73356
[startup+1090.59 s]
Raw data (loadavg): 1.04 1.03 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 17796 0 0 0 109015 54 0 0 25 0 1 0 423591671 75771904 17774 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18499 17774 603 41 0 18458 0
vsize: 73996
[startup+1100.59 s]
Raw data (loadavg): 1.04 1.03 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 17947 0 0 0 110014 55 0 0 25 0 1 0 423591671 76300288 17925 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18628 17925 603 41 0 18587 0
vsize: 74512
[startup+1110.59 s]
Raw data (loadavg): 1.03 1.03 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18030 0 0 0 111014 55 0 0 25 0 1 0 423591671 76693504 18008 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18008 603 41 0 18683 0
vsize: 74896
[startup+1120.59 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 112014 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
[startup+1130.59 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 113015 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
[startup+1140.59 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 114015 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
[startup+1150.59 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 115015 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
[startup+1160.59 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 116015 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
[startup+1170.59 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 117016 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
[startup+1180.59 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 118016 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
[startup+1190.59 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 119016 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
[startup+1200.59 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26808
Raw data (stat): 26753 (minisat+) R 26752 20937 20936 0 -1 0 18031 0 0 0 120016 55 0 0 25 0 1 0 423591671 76693504 18009 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 18009 603 41 0 18683 0
vsize: 74896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.63 s]
Raw data (loadavg): 1.00 1.02 0.95 1/54 26808
Raw data (stat): 26753 (minisat+) Z 26752 20937 20936 0 -1 12 18034 0 0 0 120016 59 0 0 25 0 1 0 423591671 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.63
CPU time (s): 1200.76
CPU user time (s): 1200.17
CPU system time (s): 0.593909
CPU usage (%): 100.011
Max. virtual memory (Kb): 74896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####