PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb45-21-opb/normalized-frb45-21-4.opb
MD5SUM	2b591d1b24a201f365bc505135aa0578
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-33
Optimality of the best value was proved	NO
Number of terms in the objective function	945
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	945
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	945
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.07
Number of variables	945
Total number of constraints	58549
Number of constraints which are clauses	58549
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 6003

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-14 02:53:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4468 boxname=wulflinc8 idbench=332 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2b591d1b24a201f365bc505135aa0578  /oldhome/oroussel/tmp/wulflinc8/normalized-frb45-21-4.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc8/normalized-frb45-21-4.opb /oldhome/oroussel/tmp/wulflinc8/normalized-frb45-21-4.opb
IDLAUNCH: 4468
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        874976 kB
Buffers:         37540 kB
Cached:         100296 kB
SwapCached:          0 kB
Active:          77632 kB
Inactive:        64880 kB
HighTotal:      131008 kB
HighFree:        25004 kB
LowTotal:       903652 kB
LowFree:        849972 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11580 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:13:29 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 4468 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58549 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   58549   117098 |   19516       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  104166   224223 |   34722       0        0     nan |  0.000 % |
c |       100 |  103642   223111 |   38194      76      983    12.9 |  0.946 % |
c |       250 |  103156   222095 |   42013     185     1779     9.6 |  1.795 % |
c |       475 |  102265   220194 |   46214     359     3317     9.2 |  3.414 % |
c |       814 |  101075   217600 |   50836     639     5778     9.0 |  5.664 % |
c |      1320 |   97538   209751 |   55920    1003    12819    12.8 | 12.575 % |
c |      2079 |   93642   200909 |   61512    1463    18801    12.9 | 20.467 % |
c |      3218 |   88661   189630 |   67663    2127    26524    12.5 | 30.497 % |
c |      4927 |   82400   175157 |   74429    3225    35325    11.0 | 43.267 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5415 |   81313   172721 |   27104    3561    38639    10.9 | 43.267 % |
c |      5515 |   81068   172126 |   29814    3614    39218    10.9 | 46.298 % |
c |      5665 |   80657   171144 |   32795    3742    40921    10.9 | 47.176 % |
c |      5890 |   79982   169546 |   36075    3902    43480    11.1 | 48.620 % |
c |      6227 |   79003   167290 |   39682    4118    45635    11.1 | 50.642 % |
c |      6733 |   78063   165079 |   43651    4430    49480    11.2 | 52.651 % |
c |      7493 |   76096   160443 |   48016    4837    55581    11.5 | 56.880 % |
c |      8632 |   74589   156885 |   52818    5773    73298    12.7 | 60.129 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9964 |   72294   151476 |   24098    6717    92845    13.8 | 60.129 % |
c |     10064 |   72294   151476 |   26507    6817    96622    14.2 | 65.090 % |
c |     10214 |   72243   151364 |   29158    6960    98656    14.2 | 65.186 % |
c |     10440 |   72148   151147 |   32074    7150   102420    14.3 | 65.368 % |
c |     10777 |   71910   150582 |   35281    7453   109836    14.7 | 65.878 % |
c |     11283 |   71431   149450 |   38810    7849   116929    14.9 | 66.893 % |
c |     12042 |   70162   146309 |   42691    8318   128370    15.4 | 69.772 % |
c |     13181 |   69233   144085 |   46960    9095   152049    16.7 | 71.811 % |
c |     14889 |   68025   141190 |   51656   10405   194546    18.7 | 74.475 % |
c |     17451 |   67465   139846 |   56821   12599   292482    23.2 | 75.681 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18058 |   67414   139655 |   22471   13154   334103    25.4 | 75.681 % |
c |     18158 |   67414   139655 |   24718   13254   340082    25.7 | 75.807 % |
c |     18309 |   67399   139620 |   27189   13361   344290    25.8 | 75.839 % |
c |     18534 |   66939   138489 |   29908   13378   346429    25.9 | 76.889 % |
c |     18872 |   66842   138270 |   32899   13666   357163    26.1 | 77.077 % |
c |     19378 |   66767   138089 |   36189   14080   377022    26.8 | 77.243 % |
c |     20137 |   66615   137726 |   39808   14759   398503    27.0 | 77.575 % |
c |     21276 |   66398   137195 |   43789   15773   445835    28.3 | 78.060 % |
c |     22984 |   66398   137195 |   48168   17481   625306    35.8 | 78.060 % |
c |     25546 |   66066   136404 |   52985   19769   794427    40.2 | 78.788 % |
c |     29390 |   65853   135895 |   58283   23401  1067190    45.6 | 79.253 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32637 |   65821   135848 |   21940   26636  1446264    54.3 | 79.253 % |
c |     32737 |   65732   135626 |   24134   26685  1448385    54.3 | 79.603 % |
c |     32887 |   65727   135615 |   26547   26818  1455138    54.3 | 79.613 % |
c |     33113 |   65727   135615 |   29202   27044  1474034    54.5 | 79.613 % |
c |     33450 |   65697   135543 |   32122   27355  1497434    54.7 | 79.680 % |
c |     33956 |   65697   135543 |   35334   27861  1538713    55.2 | 79.680 % |
c |     34715 |   65589   135270 |   38868   28521  1585884    55.6 | 79.931 % |
c |     35855 |   65482   135009 |   42754   29577  1655703    56.0 | 80.169 % |
c |     37563 |   65482   135009 |   47030   31285  1797921    57.5 | 80.169 % |
c |     40127 |   65243   134410 |   51733   33432  1984818    59.4 | 80.735 % |
c |     43971 |   64998   133825 |   56906   36983  2317054    62.7 | 81.263 % |
c |     49737 |   64814   133363 |   62597   42396  2877508    67.9 | 81.692 % |
c |     58388 |   64619   132884 |   68857   50672  3796235    74.9 | 82.131 % |
c |     71362 |   64480   132543 |   75742   63342  5261377    83.1 | 82.449 % |
c |     90823 |   64425   132404 |   83317   82608  8035630    97.3 | 82.582 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109905 |   64414   132357 |   21471  101407 10380699   102.4 | 82.582 % |
c |    110006 |   64386   132284 |   23618   21811  1640548    75.2 | 82.679 % |
c |    110156 |   64386   132284 |   25979   21961  1645897    74.9 | 82.679 % |
c |    110381 |   64386   132284 |   28577   22186  1658364    74.7 | 82.679 % |
c |    110718 |   64386   132284 |   31435   22523  1685423    74.8 | 82.679 % |
c |    111224 |   64384   132278 |   34579   23001  1726413    75.1 | 82.685 % |
c |    111983 |   64356   132212 |   38037   23758  1797994    75.7 | 82.745 % |
c |    113124 |   64356   132212 |   41840   24899  1928522    77.5 | 82.745 % |
c |    114832 |   64356   132212 |   46024   26607  2074157    78.0 | 82.745 % |
c |    117394 |   64321   132129 |   50627   29164  2294029    78.7 | 82.822 % |
c |    121238 |   64321   132129 |   55690   33008  2737094    82.9 | 82.822 % |
c |    127004 |   64317   132119 |   61259   38771  3371390    87.0 | 82.831 % |
c |    135653 |   64295   132065 |   67385   47415  4522685    95.4 | 82.882 % |
c |    148627 |   64254   131966 |   74123   60336  6178176   102.4 | 82.974 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    163149 |   64183   131807 |   21394   74787  7692198   102.9 | 82.974 % |
c |    163249 |   64183   131807 |   23533   20074  1358818    67.7 | 83.143 % |
c |    163399 |   64183   131807 |   25886   20224  1366314    67.6 | 83.143 % |
c |    163625 |   64183   131807 |   28475   20450  1379110    67.4 | 83.143 % |
c |    163962 |   64183   131807 |   31322   20787  1392044    67.0 | 83.143 % |
c |    164468 |   64183   131807 |   34455   21293  1434386    67.4 | 83.143 % |
c |    165229 |   64153   131727 |   37900   22051  1483457    67.3 | 83.222 % |
c |    166369 |   64153   131727 |   41690   23191  1600656    69.0 | 83.222 % |
c |    168077 |   64134   131680 |   45859   24890  1783760    71.7 | 83.267 % |
c |    170639 |   64102   131604 |   50445   27431  2021386    73.7 | 83.337 % |
c |    174484 |   64099   131597 |   55490   31274  2339999    74.8 | 83.343 % |
c |    180250 |   64099   131597 |   61039   37040  2928223    79.1 | 83.343 % |
c |    188899 |   64034   131440 |   67143   45638  3846777    84.3 | 83.489 % |
c |    201873 |   63981   131315 |   73857   58555  5634637    96.2 | 83.603 % |
c |    221334 |   63975   131301 |   81243   78014  7981254   102.3 | 83.616 % |
c |    250528 |   63908   131132 |   89368  107123 11438473   106.8 | 83.778 % |
c |    294319 |   63902   131118 |   98304   53229  4759432    89.4 | 83.791 % |
c |    360004 |   63735   130700 |  108135  118856 12406551   104.4 | 84.188 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 C801 -C800 -C799 -C798 -C797 -C796 C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 C657 -C656 -C655 -C654 -C653 -C652 C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 C551 -C550 -C549 -C548 -C547 -C546 -C545 C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 C421 C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 C317 -C316 -C315 -C314 -C313 -C312 -C311 C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 32678
Raw data (stat): 32678 (runsolver) R 32677 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 409356558 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0011 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 3611 0 0 0 986 13 0 0 25 0 1 0 409356558 16494592 3589 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4027 3589 603 41 0 3986 0
vsize: 16108
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 3622 0 0 0 1985 13 0 0 25 0 1 0 409356558 16494592 3600 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4027 3600 603 41 0 3986 0
vsize: 16108
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 3630 0 0 0 2985 14 0 0 25 0 1 0 409356558 16494592 3608 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4027 3608 603 41 0 3986 0
vsize: 16108
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 3721 0 0 0 3984 14 0 0 25 0 1 0 409356558 17211392 3699 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4202 3699 603 41 0 4161 0
vsize: 16808
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 3761 0 0 0 4983 15 0 0 25 0 1 0 409356558 17346560 3739 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4235 3739 603 41 0 4194 0
vsize: 16940
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 4010 0 0 0 5982 16 0 0 25 0 1 0 409356558 18386944 3988 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4489 3988 603 41 0 4448 0
vsize: 17956
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 4504 0 0 0 6980 18 0 0 25 0 1 0 409356558 20480000 4482 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5000 4482 603 41 0 4959 0
vsize: 20000
[startup+80.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 5107 0 0 0 7977 21 0 0 25 0 1 0 409356558 22896640 5085 4294967295 134512640 134672761 3221224560 3221223664 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5590 5085 603 41 0 5549 0
vsize: 22360
[startup+90.0053 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 5578 0 0 0 8975 23 0 0 25 0 1 0 409356558 24780800 5556 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6050 5556 603 41 0 6009 0
vsize: 24200
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 5956 0 0 0 9973 25 0 0 25 0 1 0 409356558 26521600 5934 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6475 5934 603 41 0 6434 0
vsize: 25900
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 6452 0 0 0 10972 26 0 0 25 0 1 0 409356558 28532736 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6966 6430 603 41 0 6925 0
vsize: 27864
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 6957 0 0 0 11970 28 0 0 25 0 1 0 409356558 30552064 6935 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7459 6935 603 41 0 7418 0
vsize: 29836
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 7437 0 0 0 12969 29 0 0 25 0 1 0 409356558 32428032 7415 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7917 7415 603 41 0 7876 0
vsize: 31668
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 7889 0 0 0 13968 30 0 0 25 0 1 0 409356558 34308096 7867 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8376 7867 603 41 0 8335 0
vsize: 33504
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 8312 0 0 0 14966 32 0 0 25 0 1 0 409356558 36048896 8290 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8801 8290 603 41 0 8760 0
vsize: 35204
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 8767 0 0 0 15963 34 0 0 25 0 1 0 409356558 37928960 8745 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9260 8745 603 41 0 9219 0
vsize: 37040
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 9194 0 0 0 16961 37 0 0 25 0 1 0 409356558 39673856 9172 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9686 9172 603 41 0 9645 0
vsize: 38744
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 9574 0 0 0 17960 38 0 0 25 0 1 0 409356558 41156608 9552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10048 9552 603 41 0 10007 0
vsize: 40192
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 9974 0 0 0 18958 40 0 0 25 0 1 0 409356558 43016192 9952 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10502 9952 603 41 0 10461 0
vsize: 42008
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 10396 0 0 0 19957 41 0 0 25 0 1 0 409356558 44744704 10374 4294967295 134512640 134672761 3221224560 3221223744 134558875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10924 10374 603 41 0 10883 0
vsize: 43696
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 10795 0 0 0 20955 43 0 0 25 0 1 0 409356558 46354432 10773 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11317 10773 603 41 0 11276 0
vsize: 45268
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 11189 0 0 0 21954 44 0 0 25 0 1 0 409356558 47951872 11167 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11167 603 41 0 11666 0
vsize: 46828
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 11562 0 0 0 22953 45 0 0 25 0 1 0 409356558 49553408 11540 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12098 11540 603 41 0 12057 0
vsize: 48392
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 11899 0 0 0 23951 47 0 0 25 0 1 0 409356558 50888704 11877 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12424 11877 603 41 0 12383 0
vsize: 49696
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 12259 0 0 0 24949 49 0 0 25 0 1 0 409356558 52355072 12237 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12782 12237 603 41 0 12741 0
vsize: 51128
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 12649 0 0 0 25947 51 0 0 25 0 1 0 409356558 53956608 12627 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13173 12627 603 41 0 13132 0
vsize: 52692
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 12996 0 0 0 26945 53 0 0 25 0 1 0 409356558 55300096 12974 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13501 12974 603 41 0 13460 0
vsize: 54004
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 13382 0 0 0 27943 54 0 0 25 0 1 0 409356558 56909824 13360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13894 13360 603 41 0 13853 0
vsize: 55576
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 13741 0 0 0 28942 56 0 0 25 0 1 0 409356558 58392576 13719 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14256 13719 603 41 0 14215 0
vsize: 57024
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14046 0 0 0 29939 58 0 0 25 0 1 0 409356558 59588608 14024 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 14024 603 41 0 14507 0
vsize: 58192
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14349 0 0 0 30938 60 0 0 25 0 1 0 409356558 60919808 14327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14873 14327 603 41 0 14832 0
vsize: 59492
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14691 0 0 0 31937 61 0 0 25 0 1 0 409356558 62251008 14669 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15198 14669 603 41 0 15157 0
vsize: 60792
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 32935 63 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 33935 63 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 34934 63 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223744 134558909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 35934 63 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 36934 64 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 37933 64 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32678
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 38933 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+400.017 s]
Raw data (loadavg): 1.15 1.00 0.92 3/57 32715
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 39932 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+410.017 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 32731
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 40932 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+420.016 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 32731
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 41932 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223744 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+430.016 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 32731
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 42932 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+440.017 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 32731
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 43933 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+450.017 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 32731
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 44933 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+460.018 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 32731
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 45933 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223744 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+470.018 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 46933 65 0 0 25 0 1 0 409356558 63410176 14949 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14949 603 41 0 15440 0
vsize: 61924
[startup+480.017 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 47933 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+490.018 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 48934 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+500.019 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 49934 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+510.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 50934 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+520.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 51934 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+530.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 52934 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+540.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 53935 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223788 134557951 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+550.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 54935 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+560.022 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 55935 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+570.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 56935 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+580.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 57935 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+590.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 58935 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+600.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 59936 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+610.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 60936 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+620.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 61936 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+630.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 62936 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+640.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 63936 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+650.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 64937 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+660.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 65937 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+670.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 66937 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+680.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 67937 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+690.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 14971 0 0 0 68938 65 0 0 25 0 1 0 409356558 63401984 14949 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15479 14949 603 41 0 15438 0
vsize: 61916
[startup+700.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32733
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 15147 0 0 0 69937 65 0 0 25 0 1 0 409356558 64069632 15125 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15642 15125 603 41 0 15601 0
vsize: 62568
[startup+710.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 15434 0 0 0 70937 66 0 0 25 0 1 0 409356558 65273856 15412 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15936 15412 603 41 0 15895 0
vsize: 63744
[startup+720.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 15731 0 0 0 71936 67 0 0 25 0 1 0 409356558 66469888 15709 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16228 15709 603 41 0 16187 0
vsize: 64912
[startup+730.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 16012 0 0 0 72936 67 0 0 25 0 1 0 409356558 67665920 15990 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16520 15990 603 41 0 16479 0
vsize: 66080
[startup+740.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 16301 0 0 0 73935 68 0 0 25 0 1 0 409356558 68878336 16279 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16816 16279 603 41 0 16775 0
vsize: 67264
[startup+750.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 16575 0 0 0 74934 69 0 0 25 0 1 0 409356558 69955584 16553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16553 603 41 0 17038 0
vsize: 68316
[startup+760.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 16797 0 0 0 75933 70 0 0 25 0 1 0 409356558 70897664 16775 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17309 16775 603 41 0 17268 0
vsize: 69236
[startup+770.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17034 0 0 0 76932 71 0 0 25 0 1 0 409356558 71831552 17012 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17537 17012 603 41 0 17496 0
vsize: 70148
[startup+780.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17228 0 0 0 77932 71 0 0 25 0 1 0 409356558 72626176 17206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17731 17206 603 41 0 17690 0
vsize: 70924
[startup+790.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17395 0 0 0 78932 72 0 0 25 0 1 0 409356558 73285632 17373 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17892 17373 603 41 0 17851 0
vsize: 71568
[startup+800.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 79931 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+810.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 80931 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+820.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 81932 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 82932 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223664 134560260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+840.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 83932 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+850.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 84932 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+860.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 85933 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+870.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 86933 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+880.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 87933 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+890.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 88933 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+900.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 89933 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+910.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 90933 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+920.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 91933 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223712 134565212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+930.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 92933 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+940.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 93934 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+950.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17516 0 0 0 94934 72 0 0 25 0 1 0 409356558 73814016 17494 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17494 603 41 0 17980 0
vsize: 72084
[startup+960.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17517 0 0 0 95934 72 0 0 25 0 1 0 409356558 73814016 17495 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17495 603 41 0 17980 0
vsize: 72084
[startup+970.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17517 0 0 0 96934 72 0 0 25 0 1 0 409356558 73814016 17495 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17495 603 41 0 17980 0
vsize: 72084
[startup+980.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17517 0 0 0 97935 72 0 0 25 0 1 0 409356558 73814016 17495 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17495 603 41 0 17980 0
vsize: 72084
[startup+990.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17517 0 0 0 98935 72 0 0 25 0 1 0 409356558 73814016 17495 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17495 603 41 0 17980 0
vsize: 72084
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17517 0 0 0 99935 72 0 0 25 0 1 0 409356558 73814016 17495 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17495 603 41 0 17980 0
vsize: 72084
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17517 0 0 0 100935 72 0 0 25 0 1 0 409356558 73814016 17495 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17495 603 41 0 17980 0
vsize: 72084
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17518 0 0 0 101935 72 0 0 25 0 1 0 409356558 73814016 17496 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17496 603 41 0 17980 0
vsize: 72084
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17518 0 0 0 102936 72 0 0 25 0 1 0 409356558 73814016 17496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17496 603 41 0 17980 0
vsize: 72084
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17518 0 0 0 103936 72 0 0 25 0 1 0 409356558 73814016 17496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17496 603 41 0 17980 0
vsize: 72084
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17518 0 0 0 104936 72 0 0 25 0 1 0 409356558 73814016 17496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17496 603 41 0 17980 0
vsize: 72084
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17518 0 0 0 105936 72 0 0 25 0 1 0 409356558 73814016 17496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17496 603 41 0 17980 0
vsize: 72084
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17518 0 0 0 106936 72 0 0 25 0 1 0 409356558 73814016 17496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17496 603 41 0 17980 0
vsize: 72084
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17518 0 0 0 107936 72 0 0 25 0 1 0 409356558 73814016 17496 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17496 603 41 0 17980 0
vsize: 72084
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17518 0 0 0 108937 72 0 0 25 0 1 0 409356558 73814016 17496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17496 603 41 0 17980 0
vsize: 72084
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17603 0 0 0 109937 73 0 0 25 0 1 0 409356558 74080256 17581 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18086 17581 603 41 0 18045 0
vsize: 72344
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 17836 0 0 0 110936 74 0 0 25 0 1 0 409356558 75149312 17814 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18347 17814 603 41 0 18306 0
vsize: 73388
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 18136 0 0 0 111935 74 0 0 25 0 1 0 409356558 76345344 18114 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18639 18114 603 41 0 18598 0
vsize: 74556
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 18423 0 0 0 112934 75 0 0 25 0 1 0 409356558 77406208 18401 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18898 18401 603 41 0 18857 0
vsize: 75592
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 18658 0 0 0 113934 76 0 0 25 0 1 0 409356558 78495744 18636 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19164 18636 603 41 0 19123 0
vsize: 76656
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 18897 0 0 0 114934 76 0 0 25 0 1 0 409356558 79437824 18875 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19394 18875 603 41 0 19353 0
vsize: 77576
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 19153 0 0 0 115933 77 0 0 25 0 1 0 409356558 81027072 19131 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19782 19131 603 41 0 19741 0
vsize: 79128
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 19390 0 0 0 116932 78 0 0 25 0 1 0 409356558 81969152 19368 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20012 19368 603 41 0 19971 0
vsize: 80048
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 19658 0 0 0 117932 79 0 0 25 0 1 0 409356558 83030016 19636 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20271 19636 603 41 0 20230 0
vsize: 81084
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 19766 0 0 0 118932 79 0 0 25 0 1 0 409356558 83562496 19744 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20401 19744 603 41 0 20360 0
vsize: 81604
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32735
Raw data (stat): 32678 (minisat+) R 32677 26667 26666 0 -1 0 19766 0 0 0 119932 79 0 0 25 0 1 0 409356558 83562496 19744 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20401 19744 603 41 0 20360 0
vsize: 81604
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 32735
Raw data (stat): 32678 (minisat+) Z 32677 26667 26666 0 -1 12 19769 0 0 0 119932 82 0 0 25 0 1 0 409356558 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.08
CPU time (s): 1200.16
CPU user time (s): 1199.33
CPU system time (s): 0.828873
CPU usage (%): 100.006
Max. virtual memory (Kb): 81604
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####