PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-14 01:00:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4091 boxname=wulflinc12 idbench=331 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b3a3f977e810fc2043ea057a8d94a7d8  /oldhome/oroussel/tmp/wulflinc12/normalized-frb45-21-3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc12/normalized-frb45-21-3.opb /oldhome/oroussel/tmp/wulflinc12/normalized-frb45-21-3.opb
IDLAUNCH: 4091
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        908608 kB
Buffers:         35496 kB
Cached:          70908 kB
SwapCached:         16 kB
Active:          62320 kB
Inactive:        46924 kB
HighTotal:      131008 kB
HighFree:        56280 kB
LowTotal:       903652 kB
LowFree:        852328 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11320 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:20:43 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 4091 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58245 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   58245   116490 |   17473       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   58245   116490 |   23298       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 2.70059 s)
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  103674   223173 |   31102       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/31066          
c   -- var.elim.:  2000/31066          
c   -- var.elim.:  3000/31066          
c   -- var.elim.:  4000/31066          
c   -- var.elim.:  5000/31066          
c   -- var.elim.:  6000/31066          
c   -- var.elim.:  7000/31066          
c   -- var.elim.:  8000/31066          
c   -- var.elim.:  9000/31066          
c   -- var.elim.:  10000/31066          
c   -- var.elim.:  11000/31066          
c   -- var.elim.:  12000/31066          
c   -- var.elim.:  13000/31066          
c   -- var.elim.:  14000/31066          
c   -- var.elim.:  15000/31066          
c   -- var.elim.:  16000/31066          
c   -- var.elim.:  17000/31066          
c   -- var.elim.:  18000/31066          
c   -- var.elim.:  19000/31066          
c   -- var.elim.:  20000/31066          
c   -- var.elim.:  21000/31066          
c   -- var.elim.:  22000/31066          
c   -- var.elim.:  23000/31066          
c   -- var.elim.:  24000/31066          
c   -- var.elim.:  25000/31066          
c   -- var.elim.:  26000/31066          
c   -- var.elim.:  27000/31066          
c   -- var.elim.:  28000/31066          
c   -- var.elim.:  29000/31066          
c   -- var.elim.:  30000/31066          
c   -- var.elim.:  31000/31066          
c   -- var.elim.:  31066/31066          
c   -- var.elim.:  1000/15761          
c   -- var.elim.:  2000/15761          
c   -- var.elim.:  3000/15761          
c   -- var.elim.:  4000/15761          
c   -- var.elim.:  5000/15761          
c   -- var.elim.:  6000/15761          
c   -- var.elim.:  7000/15761          
c   -- var.elim.:  8000/15761          
c   -- var.elim.:  9000/15761          
c   -- var.elim.:  10000/15761          
c   -- var.elim.:  11000/15761          
c   -- var.elim.:  12000/15761          
c   -- var.elim.:  13000/15761          
c   -- var.elim.:  14000/15761          
c   -- var.elim.:  15000/15761          
c   -- var.elim.:  15761/15761          
c   -- var.elim.:  1000/3180          
c   -- var.elim.:  2000/3180          
c   -- var.elim.:  3000/3180          
c   -- var.elim.:  3180/3180          
c   -- subsuming                       
c   -- var.elim.:  1000/6193          
c   -- var.elim.:  2000/6193          
c   -- var.elim.:  3000/6193          
c   -- var.elim.:  4000/6193          
c   -- var.elim.:  5000/6193          
c   -- var.elim.:  6000/6193          
c   -- var.elim.:  6193/6193          
c   -- var.elim.:  405/405          
c   -- subsuming                       
c |         0 |   71477   222266 |      --       0       --      -- |     --   | -32197/-906
c |         0 |   71477   222266 |   28590       0        0     nan |  0.000 % |
c |       100 |   71477   222266 |   31449     100    10118   101.2 | 53.101 % |
c |       250 |   71477   222266 |   34594     250    39554   158.2 | 53.101 % |
c |       475 |   71477   222266 |   38054     475    84024   176.9 | 53.101 % |
c |       812 |   71477   222266 |   41859     812   136948   168.7 | 53.101 % |
c ==============================================================================
c (current CPU-time: 77.9931 s)
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1130 |   78027   239668 |   23408    1125   195795   174.0 | 53.101 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12689          
c   -- var.elim.:  2000/12689          
c   -- var.elim.:  3000/12689          
c   -- var.elim.:  4000/12689          
c   -- var.elim.:  5000/12689          
c   -- var.elim.:  6000/12689          
c   -- var.elim.:  7000/12689          
c   -- var.elim.:  8000/12689          
c   -- var.elim.:  9000/12689          
c   -- var.elim.:  10000/12689          
c   -- var.elim.:  11000/12689          
c   -- var.elim.:  12000/12689          
c   -- var.elim.:  12689/12689          
c   -- var.elim.:  1000/4631          
c   -- var.elim.:  2000/4631          
c   -- var.elim.:  3000/4631          
c   -- var.elim.:  4000/4631          
c   -- var.elim.:  4631/4631          
c   -- var.elim.:  225/225          
c   -- subsuming                       
c   -- var.elim.:  1000/4648          
c   -- var.elim.:  2000/4648          
c   -- var.elim.:  3000/4648          
c   -- var.elim.:  4000/4648          
c   -- var.elim.:  4648/4648          
c   -- var.elim.:  310/310          
c |      1130 |   71558   232035 |      --    1125       --      -- |     --   | -6448/-6941
c |      1130 |   71558   232035 |   28623    1037   129136   124.5 | 53.101 % |
c |      1232 |   71558   232035 |   31485    1139   140406   123.3 | 62.561 % |
c |      1382 |   71558   232035 |   34634    1289   181590   140.9 | 62.562 % |
c |      1607 |   71558   232035 |   38097    1514   208290   137.6 | 62.562 % |
c |      1944 |   71558   232035 |   41907    1851   255350   138.0 | 62.561 % |
c |      2450 |   71337   229881 |   45955    2342   327407   139.8 | 63.099 % |
c |      3209 |   71161   228051 |   50426    3086   461095   149.4 | 63.545 % |
c |      4348 |   71003   226552 |   55345    4202   667161   158.8 | 63.915 % |
c |      6056 |   70772   224489 |   60682    5871   992569   169.1 | 64.452 % |
c ==============================================================================
c (current CPU-time: 121.083 s)
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6632 |   75184   236452 |   22555    6438  1154995   179.4 | 64.452 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11059          
c   -- var.elim.:  2000/11059          
c   -- var.elim.:  3000/11059          
c   -- var.elim.:  4000/11059          
c   -- var.elim.:  5000/11059          
c   -- var.elim.:  6000/11059          
c   -- var.elim.:  7000/11059          
c   -- var.elim.:  8000/11059          
c   -- var.elim.:  9000/11059          
c   -- var.elim.:  10000/11059          
c   -- var.elim.:  11000/11059          
c   -- var.elim.:  11059/11059          
c   -- var.elim.:  1000/3458          
c   -- var.elim.:  2000/3458          
c   -- var.elim.:  3000/3458          
c   -- var.elim.:  3458/3458          
c |      6632 |   70796   228603 |      --    6438       --      -- |     --   | -4387/-7846
c |      6632 |   70796   228603 |   28318    6436  1154850   179.4 | 64.452 % |
c |      6732 |   70796   228603 |   31150    6536  1171715   179.3 | 64.907 % |
c |      6882 |   70796   228603 |   34265    6686  1201178   179.7 | 64.907 % |
c |      7107 |   70758   228264 |   37671    6909  1237965   179.2 | 64.987 % |
c |      7444 |   70696   227650 |   41402    7232  1290240   178.4 | 65.142 % |
c |      7950 |   70660   227297 |   45519    7736  1388325   179.5 | 65.232 % |
c |      8710 |   70558   226281 |   49999    8481  1516441   178.8 | 65.487 % |
c |      9850 |   70458   225366 |   54921    9591  1726274   180.0 | 65.738 % |
c |     11558 |   70358   224396 |   60327   11292  2167733   192.0 | 65.988 % |
c ==============================================================================
c (current CPU-time: 154.207 s)
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13640 |   77010   241700 |   23102   13333  2696880   202.3 | 65.988 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13319          
c   -- var.elim.:  2000/13319          
c   -- var.elim.:  3000/13319          
c   -- var.elim.:  4000/13319          
c   -- var.elim.:  5000/13319          
c   -- var.elim.:  6000/13319          
c   -- var.elim.:  7000/13319          
c   -- var.elim.:  8000/13319          
c   -- var.elim.:  9000/13319          
c   -- var.elim.:  10000/13319          
c   -- var.elim.:  11000/13319          
c   -- var.elim.:  12000/13319          
c   -- var.elim.:  13000/13319          
c   -- var.elim.:  13319/13319          
c   -- var.elim.:  1000/4961          
c   -- var.elim.:  2000/4961          
c   -- var.elim.:  3000/4961          
c   -- var.elim.:  4000/4961          
c   -- var.elim.:  4961/4961          
c   -- var.elim.:  4/4          
c |     13640 |   70337   229253 |      --   13333       --      -- |     --   | -6667/-12434
c |     13640 |   70337   229253 |   28134   13326  2696857   202.4 | 65.988 % |
c |     13740 |   70337   229253 |   30948   13426  2710923   201.9 | 67.390 % |
c |     13893 |   70337   229253 |   34043   13579  2749825   202.5 | 67.390 % |
c |     14119 |   70337   229253 |   37447   13805  2815533   204.0 | 67.390 % |
c |     14456 |   70313   229044 |   41178   14141  2896684   204.8 | 67.448 % |
c |     14962 |   70275   228633 |   45271   14638  3015608   206.0 | 67.540 % |
c |     15721 |   70275   228633 |   49798   15397  3226129   209.5 | 67.539 % |
c |     16861 |   70275   228633 |   54778   16537  3522344   213.0 | 67.540 % |
c |     18570 |   70169   227624 |   60165   18200  3955844   217.4 | 67.795 % |
c |     21132 |   69685   223101 |   65725   20639  4605882   223.2 | 68.955 % |
c |     24976 |   69433   220638 |   72036   24397  5671504   232.5 | 69.561 % |
c |     30742 |   69040   216890 |   78791   30069  7591028   252.5 | 70.505 % |
c |     39391 |   68598   212730 |   86115   38534 10257058   266.2 | 71.535 % |
c ==============================================================================
c (current CPU-time: 300.283 s)
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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     45150 |   69382   213219 |   20814   44241 12135846   274.3 | 71.535 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6799          
c   -- var.elim.:  2000/6799          
c   -- var.elim.:  3000/6799          
c   -- var.elim.:  4000/6799          
c   -- var.elim.:  5000/6799          
c   -- var.elim.:  6000/6799          
c   -- var.elim.:  6799/6799          
c   -- var.elim.:  1000/2029          
c   -- var.elim.:  2000/2029          
c   -- var.elim.:  2029/2029          
c |     45150 |   68321   206672 |      --   44241       --      -- |     --   | -1042/-2025
c |     45150 |   68321   206672 |   27328   36880  5991933   162.5 | 71.535 % |
c |     45250 |   68291   206378 |   30048   36979  6015707   162.7 | 72.350 % |
c |     45400 |   68257   206061 |   33036   37128  6055883   163.1 | 72.422 % |
c |     45625 |   68257   206061 |   36340   37353  6113868   163.7 | 72.422 % |
c |     45962 |   68257   206061 |   39974   37690  6211218   164.8 | 72.422 % |
c |     46468 |   68255   206040 |   43970   38159  6321726   165.7 | 72.427 % |
c |     47227 |   68255   206040 |   48367   38918  6528928   167.8 | 72.427 % |
c |     48366 |   68253   206020 |   53202   40054  6787018   169.4 | 72.432 % |
c |     50076 |   68253   206020 |   58522   41764  7343192   175.8 | 72.432 % |
c |     52638 |   68189   205399 |   64314   44313  8028763   181.2 | 72.576 % |
c |     56482 |   68082   204482 |   70634   48088  9128601   189.8 | 72.817 % |
c |     62248 |   67959   202784 |   77557   53774 10764763   200.2 | 73.096 % |
c |     70897 |   67706   200381 |   84996   62228 13437337   215.9 | 73.673 % |
c |     83871 |   67586   199278 |   93330   75145 17729616   235.9 | 73.952 % |
c |    103332 |   66946   193479 |  101690   94379 23867743   252.9 | 75.458 % |
c |    132526 |   66592   190252 |  111268   29687  6384491   215.1 | 76.272 % |
c |    176315 |   66117   186054 |  121522   73371 20839104   284.0 | 77.388 % |
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 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163#### 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.90 0.97 0.91 2/54 29925
Raw data (stat): 29925 (runsolver) R 29924 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422241305 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 29925
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 6439 0 0 0 972 26 0 0 25 0 1 0 422241305 26619904 6027 4294967295 134512640 134672761 3221224560 3221223056 134644251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6499 6027 603 41 0 6458 0
vsize: 25996
[startup+20.0003 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 29925
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 6442 0 0 0 1973 26 0 0 25 0 1 0 422241305 26619904 6030 4294967295 134512640 134672761 3221224560 3221222288 134566560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6499 6030 603 41 0 6458 0
vsize: 25996
[startup+30.0011 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 29925
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 6452 0 0 0 2973 26 0 0 25 0 1 0 422241305 26783744 6040 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6539 6040 603 41 0 6498 0
vsize: 26156
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29925
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 6475 0 0 0 3973 26 0 0 25 0 1 0 422241305 26783744 6063 4294967295 134512640 134672761 3221224560 3221222492 134566513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6539 6063 603 41 0 6498 0
vsize: 26156
[startup+50.0022 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 6483 0 0 0 4973 26 0 0 25 0 1 0 422241305 26783744 6071 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6539 6071 603 41 0 6498 0
vsize: 26156
[startup+60.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 6483 0 0 0 5972 26 0 0 25 0 1 0 422241305 26783744 6071 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6539 6071 603 41 0 6498 0
vsize: 26156
[startup+70.0018 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 6687 0 0 0 6972 26 0 0 25 0 1 0 422241305 27766784 6275 4294967295 134512640 134672761 3221224560 3221223104 134621095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6779 6275 603 41 0 6738 0
vsize: 27116
[startup+80.0024 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 8318 0 0 0 7966 32 0 0 25 0 1 0 422241305 32788480 6979 4294967295 134512640 134672761 3221224560 3221223104 134621090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8005 6979 603 41 0 7964 0
vsize: 32020
[startup+90.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 8318 0 0 0 8950 49 0 0 25 0 1 0 422241305 31133696 6775 4294967295 134512640 134672761 3221224560 3221223008 134643612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7601 6775 603 41 0 7560 0
vsize: 30404
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 8522 0 0 0 9949 49 0 0 25 0 1 0 422241305 32796672 6979 4294967295 134512640 134672761 3221224560 3221223024 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8007 6979 603 41 0 7966 0
vsize: 32028
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 8522 0 0 0 10950 49 0 0 25 0 1 0 422241305 31133696 6775 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7601 6775 603 41 0 7560 0
vsize: 30404
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 8958 0 0 0 11949 50 0 0 25 0 1 0 422241305 33107968 7211 4294967295 134512640 134672761 3221224560 3221223600 134614246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8083 7211 603 41 0 8042 0
vsize: 32332
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 10791 0 0 0 12912 74 0 0 25 0 1 0 422241305 34045952 7533 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8312 7533 603 41 0 8271 0
vsize: 33248
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 10986 0 0 0 13912 74 0 0 25 0 1 0 422241305 34963456 7728 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8536 7728 603 41 0 8495 0
vsize: 34144
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 11860 0 0 0 14909 77 0 0 25 0 1 0 422241305 38490112 8602 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9397 8602 603 41 0 9356 0
vsize: 37588
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 14321 0 0 0 15892 94 0 0 25 0 1 0 422241305 40984576 9329 4294967295 134512640 134672761 3221224560 3221222976 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10006 9329 603 41 0 9965 0
vsize: 40024
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 14321 0 0 0 16877 109 0 0 25 0 1 0 422241305 40984576 9329 4294967295 134512640 134672761 3221224560 3221223008 134643532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10006 9329 603 41 0 9965 0
vsize: 40024
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 14900 0 0 0 17875 110 0 0 25 0 1 0 422241305 43282432 9908 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10567 9908 603 41 0 10526 0
vsize: 42268
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 15674 0 0 0 18873 112 0 0 25 0 1 0 422241305 46583808 10682 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11373 10682 603 41 0 11332 0
vsize: 45492
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 16201 0 0 0 19872 113 0 0 25 0 1 0 422241305 48680960 11209 4294967295 134512640 134672761 3221224560 3221223696 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11885 11209 603 41 0 11844 0
vsize: 47540
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 17067 0 0 0 20871 115 0 0 25 0 1 0 422241305 52174848 12075 4294967295 134512640 134672761 3221224560 3221223732 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12738 12075 603 41 0 12697 0
vsize: 50952
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 17889 0 0 0 21869 117 0 0 25 0 1 0 422241305 55541760 12897 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13560 12897 603 41 0 13519 0
vsize: 54240
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 18810 0 0 0 22867 119 0 0 25 0 1 0 422241305 59314176 13818 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14481 13818 603 41 0 14440 0
vsize: 57924
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 19758 0 0 0 23865 122 0 0 25 0 1 0 422241305 63209472 14766 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15432 14766 603 41 0 15391 0
vsize: 61728
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 20392 0 0 0 24863 123 0 0 25 0 1 0 422241305 65966080 15400 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16105 15400 603 41 0 16064 0
vsize: 64420
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 21128 0 0 0 25861 126 0 0 25 0 1 0 422241305 68960256 16136 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16836 16136 603 41 0 16795 0
vsize: 67344
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 21787 0 0 0 26860 127 0 0 25 0 1 0 422241305 71675904 16795 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17499 16795 603 41 0 17458 0
vsize: 69996
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 22669 0 0 0 27859 128 0 0 25 0 1 0 422241305 75231232 17677 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18367 17677 603 41 0 18326 0
vsize: 73468
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 23131 0 0 0 28859 129 0 0 25 0 1 0 422241305 77189120 18139 4294967295 134512640 134672761 3221224560 3221223600 134614335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18845 18139 603 41 0 18804 0
vsize: 75380
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29927
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 23911 0 0 0 29857 130 0 0 25 0 1 0 422241305 80306176 18919 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19606 18919 603 41 0 19565 0
vsize: 78424
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26296 0 0 0 30836 151 0 0 25 0 1 0 422241305 80764928 19062 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19718 19062 603 41 0 19677 0
vsize: 78872
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26296 0 0 0 31836 151 0 0 25 0 1 0 422241305 80748544 19058 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19058 603 41 0 19673 0
vsize: 78856
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26296 0 0 0 32837 151 0 0 25 0 1 0 422241305 80748544 19058 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19058 603 41 0 19673 0
vsize: 78856
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26296 0 0 0 33837 151 0 0 25 0 1 0 422241305 80748544 19058 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19058 603 41 0 19673 0
vsize: 78856
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26297 0 0 0 34837 151 0 0 25 0 1 0 422241305 80748544 19059 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19059 603 41 0 19673 0
vsize: 78856
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26299 0 0 0 35837 151 0 0 25 0 1 0 422241305 80748544 19061 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19061 603 41 0 19673 0
vsize: 78856
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26301 0 0 0 36837 151 0 0 25 0 1 0 422241305 80748544 19063 4294967295 134512640 134672761 3221224560 3221223744 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19063 603 41 0 19673 0
vsize: 78856
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26303 0 0 0 37838 151 0 0 25 0 1 0 422241305 80748544 19065 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19065 603 41 0 19673 0
vsize: 78856
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26305 0 0 0 38838 151 0 0 25 0 1 0 422241305 80748544 19067 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19067 603 41 0 19673 0
vsize: 78856
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26307 0 0 0 39838 151 0 0 25 0 1 0 422241305 80748544 19069 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 19069 603 41 0 19673 0
vsize: 78856
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26344 0 0 0 40838 151 0 0 25 0 1 0 422241305 81002496 19106 4294967295 134512640 134672761 3221224560 3221223704 134616108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19776 19106 603 41 0 19735 0
vsize: 79104
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 26947 0 0 0 41837 153 0 0 25 0 1 0 422241305 83374080 19709 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20355 19709 603 41 0 20314 0
vsize: 81420
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 27524 0 0 0 42836 154 0 0 25 0 1 0 422241305 85749760 20286 4294967295 134512640 134672761 3221224560 3221223432 1075352749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20935 20286 603 41 0 20894 0
vsize: 83740
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 27820 0 0 0 43835 155 0 0 25 0 1 0 422241305 86937600 20582 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21225 20582 603 41 0 21184 0
vsize: 84900
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 28284 0 0 0 44834 156 0 0 25 0 1 0 422241305 88903680 21046 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21705 21046 603 41 0 21664 0
vsize: 86820
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 28886 0 0 0 45832 158 0 0 25 0 1 0 422241305 91402240 21648 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22315 21648 603 41 0 22274 0
vsize: 89260
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 29715 0 0 0 46831 160 0 0 25 0 1 0 422241305 94920704 22477 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23174 22477 603 41 0 23133 0
vsize: 92696
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 30377 0 0 0 47829 161 0 0 25 0 1 0 422241305 97656832 23139 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23842 23139 603 41 0 23801 0
vsize: 95368
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 31174 0 0 0 48828 163 0 0 25 0 1 0 422241305 100937728 23936 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24643 23936 603 41 0 24602 0
vsize: 98572
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 31765 0 0 0 49826 165 0 0 25 0 1 0 422241305 103391232 24527 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25242 24527 603 41 0 25201 0
vsize: 100968
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 32188 0 0 0 50825 166 0 0 25 0 1 0 422241305 105103360 24950 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25660 24950 603 41 0 25619 0
vsize: 102640
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 32563 0 0 0 51825 166 0 0 25 0 1 0 422241305 106565632 25325 4294967295 134512640 134672761 3221224560 3221223408 134604610 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26017 25325 603 41 0 25976 0
vsize: 104068
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 33075 0 0 0 52824 167 0 0 25 0 1 0 422241305 108662784 25837 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26529 25837 603 41 0 26488 0
vsize: 106116
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 33502 0 0 0 53823 169 0 0 25 0 1 0 422241305 110510080 26264 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26980 26264 603 41 0 26939 0
vsize: 107920
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 33894 0 0 0 54822 170 0 0 25 0 1 0 422241305 112062464 26656 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27359 26656 603 41 0 27318 0
vsize: 109436
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 34338 0 0 0 55820 172 0 0 25 0 1 0 422241305 113881088 27100 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27803 27100 603 41 0 27762 0
vsize: 111212
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 34772 0 0 0 56819 173 0 0 25 0 1 0 422241305 115687424 27534 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28244 27534 603 41 0 28203 0
vsize: 112976
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 35187 0 0 0 57819 174 0 0 25 0 1 0 422241305 117268480 27949 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28630 27949 603 41 0 28589 0
vsize: 114520
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 35530 0 0 0 58818 175 0 0 25 0 1 0 422241305 118718464 28292 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28984 28292 603 41 0 28943 0
vsize: 115936
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 35877 0 0 0 59817 176 0 0 25 0 1 0 422241305 120180736 28639 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29341 28639 603 41 0 29300 0
vsize: 117364
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 36249 0 0 0 60816 177 0 0 25 0 1 0 422241305 121610240 29011 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29690 29011 603 41 0 29649 0
vsize: 118760
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 36784 0 0 0 61815 178 0 0 25 0 1 0 422241305 123826176 29546 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30231 29546 603 41 0 30190 0
vsize: 120924
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 37581 0 0 0 62813 181 0 0 25 0 1 0 422241305 127082496 30343 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31026 30343 603 41 0 30985 0
vsize: 124104
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 37791 0 0 0 63812 181 0 0 25 0 1 0 422241305 127995904 30553 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31249 30553 603 41 0 31208 0
vsize: 124996
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 38145 0 0 0 64812 182 0 0 25 0 1 0 422241305 129409024 30907 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31594 30907 603 41 0 31553 0
vsize: 126376
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 38564 0 0 0 65811 183 0 0 25 0 1 0 422241305 131117056 31326 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32011 31326 603 41 0 31970 0
vsize: 128044
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 38900 0 0 0 66810 184 0 0 25 0 1 0 422241305 132452352 31662 4294967295 134512640 134672761 3221224560 3221223704 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32337 31662 603 41 0 32296 0
vsize: 129348
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 39244 0 0 0 67809 185 0 0 25 0 1 0 422241305 133898240 32006 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32690 32006 603 41 0 32649 0
vsize: 130760
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 39733 0 0 0 68808 186 0 0 25 0 1 0 422241305 135868416 32495 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33171 32495 603 41 0 33130 0
vsize: 132684
[startup+700.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 40232 0 0 0 69808 187 0 0 25 0 1 0 422241305 137981952 32994 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33687 32994 603 41 0 33646 0
vsize: 134748
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 40564 0 0 0 70807 188 0 0 25 0 1 0 422241305 139309056 33326 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34011 33326 603 41 0 33970 0
vsize: 136044
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 41066 0 0 0 71805 190 0 0 25 0 1 0 422241305 141377536 33828 4294967295 134512640 134672761 3221224560 3221223600 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34516 33828 603 41 0 34475 0
vsize: 138064
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 41312 0 0 0 72804 191 0 0 25 0 1 0 422241305 142438400 34074 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34775 34074 603 41 0 34734 0
vsize: 139100
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 41737 0 0 0 73803 192 0 0 25 0 1 0 422241305 144142336 34499 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35191 34499 603 41 0 35150 0
vsize: 140764
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 42050 0 0 0 74802 193 0 0 25 0 1 0 422241305 145330176 34812 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35481 34812 603 41 0 35440 0
vsize: 141924
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 42349 0 0 0 75802 194 0 0 25 0 1 0 422241305 146677760 35111 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35810 35111 603 41 0 35769 0
vsize: 143240
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 42711 0 0 0 76801 195 0 0 25 0 1 0 422241305 148111360 35473 4294967295 134512640 134672761 3221224560 3221223704 134616189 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36160 35473 603 41 0 36119 0
vsize: 144640
[startup+780.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 43164 0 0 0 77800 196 0 0 25 0 1 0 422241305 149921792 35926 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36602 35926 603 41 0 36561 0
vsize: 146408
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 43552 0 0 0 78800 197 0 0 25 0 1 0 422241305 151502848 36314 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36988 36314 603 41 0 36947 0
vsize: 147952
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 44052 0 0 0 79799 198 0 0 25 0 1 0 422241305 153600000 36814 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37500 36814 603 41 0 37459 0
vsize: 150000
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 44574 0 0 0 80797 200 0 0 25 0 1 0 422241305 155709440 37336 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38015 37336 603 41 0 37974 0
vsize: 152060
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 44885 0 0 0 81797 200 0 0 25 0 1 0 422241305 157036544 37647 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38339 37647 603 41 0 38298 0
vsize: 153356
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 45421 0 0 0 82796 202 0 0 25 0 1 0 422241305 159170560 38183 4294967295 134512640 134672761 3221224560 3221223744 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38860 38183 603 41 0 38819 0
vsize: 155440
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 45702 0 0 0 83795 203 0 0 25 0 1 0 422241305 160366592 38464 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39152 38464 603 41 0 39111 0
vsize: 156608
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 46126 0 0 0 84795 203 0 0 25 0 1 0 422241305 162033664 38888 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39559 38888 603 41 0 39518 0
vsize: 158236
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 46658 0 0 0 85793 204 0 0 25 0 1 0 422241305 164253696 39420 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40101 39420 603 41 0 40060 0
vsize: 160404
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47104 0 0 0 86792 206 0 0 25 0 1 0 422241305 166080512 39866 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40547 39866 603 41 0 40506 0
vsize: 162188
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 87792 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 88792 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 89792 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 90792 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 91792 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 92793 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 93793 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 94793 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 95793 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 96793 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 97794 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 98794 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 99794 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 100794 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 101794 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 102794 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 103795 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 104795 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 105795 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 106795 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223704 134616154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 107795 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 108796 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 109796 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 110796 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 111796 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223748 134610770 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 112796 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 113797 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 114797 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 115797 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 116797 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 117797 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 118798 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29929
Raw data (stat): 29925 (minisat+) R 29924 25285 25284 0 -1 0 47496 0 0 0 119798 206 0 0 25 0 1 0 422241305 167153664 40110 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 40110 603 41 0 40768 0
vsize: 163236
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29929
Raw data (stat): 29925 (minisat+) Z 29924 25285 25284 0 -1 12 47497 0 0 0 119798 217 0 0 25 0 1 0 422241305 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.15
CPU time (s): 1200.16
CPU user time (s): 1197.98
CPU system time (s): 2.17367
CPU usage (%): 100.001
Max. virtual memory (Kb): 163236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####