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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-4.opb
MD5SUMb85a90571dde4fe12541342d5605d680
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -37
Optimality of the best value was proved NO
Number of terms in the objective function 1150
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 1150
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1150
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.1
Number of variables1150
Total number of constraints80258
Number of constraints which are clauses80258
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 6382

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        716072 kB
Buffers:         38340 kB
Cached:         239236 kB
SwapCached:          0 kB
Active:          86584 kB
Inactive:       193828 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        715820 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32496 kB
Committed_AS:    63456 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:07:47 (client local time) WITH STATUS 10 IN 1200.57 SECONDS
stats: 4849 7 1200.57 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80258 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   80258   160516 |   26752       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -36
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  216594   479496 |   72198       0        0     nan |  0.000 % |
c |       100 |  216441   479151 |   79417      96     1104    11.5 |  0.151 % |
c |       250 |  213994   473557 |   87359     207     2004     9.7 |  1.675 % |
c |       476 |  211320   467433 |   96095     376     2848     7.6 |  3.412 % |
c |       813 |  206061   455387 |  105705     606     4582     7.6 |  6.836 % |
c |      1319 |  199175   439525 |  116275     965     7899     8.2 | 11.488 % |
c |      2078 |  187119   411696 |  127903    1488    11679     7.8 | 19.741 % |
c |      3217 |  175158   384044 |  140693    2363    19778     8.4 | 27.979 % |
c |      4925 |  156831   341370 |  154762    3542    30633     8.6 | 40.913 % |
c |      7487 |  134804   289667 |  170239    4866    44588     9.2 | 57.019 % |
c ==============================================================================
c Found solution: -37
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11068 |  111914   236034 |   37304    6353    66451    10.5 | 57.019 % |
c |     11169 |  111910   236025 |   41034    6451    68189    10.6 | 74.103 % |
c |     11320 |  111259   234503 |   45137    6460    67942    10.5 | 74.583 % |
c |     11546 |  110550   232850 |   49651    6638    69331    10.4 | 75.102 % |
c |     11883 |  110126   231863 |   54616    6900    71932    10.4 | 75.403 % |
c ==============================================================================
c Found solution: -38
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12311 |  109741   230917 |   36580    7227    78544    10.9 | 75.403 % |
c |     12411 |  109581   230540 |   40238    7302    78889    10.8 | 75.795 % |
c |     12562 |  108978   229139 |   44261    7397    79922    10.8 | 76.213 % |
c |     12787 |  108578   228201 |   48687    7565    81312    10.7 | 76.509 % |
c |     13127 |  107949   226714 |   53556    7781    83946    10.8 | 76.989 % |
c |     13633 |  107494   225645 |   58912    8228    89532    10.9 | 77.328 % |
c |     14392 |  106694   223767 |   64803    8778   101094    11.5 | 77.912 % |
c ==============================================================================
c Found solution: -39
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14793 |  106554   223476 |   35518    9028   109877    12.2 | 77.912 % |
c |     14893 |  106110   222432 |   39069    9115   110486    12.1 | 78.444 % |
c |     15043 |  106110   222432 |   42976    9265   112901    12.2 | 78.444 % |
c |     15268 |  105527   221055 |   47274    9372   114033    12.2 | 78.892 % |
c |     15606 |  105098   220061 |   52001    9694   118086    12.2 | 79.190 % |
c |     16112 |  105023   219888 |   57202   10159   125116    12.3 | 79.298 % |
c ==============================================================================
c Found solution: -40
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16371 |  104413   218436 |   34804   10148   126676    12.5 | 79.298 % |
c |     16471 |  104157   217850 |   38284   10241   127543    12.5 | 79.873 % |
c |     16622 |  104157   217850 |   42112   10392   129445    12.5 | 79.873 % |
c |     16847 |  103585   216522 |   46324   10531   131495    12.5 | 80.276 % |
c |     17184 |  103126   215459 |   50956   10716   133577    12.5 | 80.595 % |
c |     17690 |  102099   213050 |   56052   11081   141592    12.8 | 81.348 % |
c |     18449 |  102099   213050 |   61657   11840   175028    14.8 | 81.348 % |
c |     19588 |  101706   212128 |   67823   12824   202387    15.8 | 81.644 % |
c |     21297 |  100386   209029 |   74605   14450   281799    19.5 | 82.643 % |
c ==============================================================================
c Found solution: -41
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22964 |  100283   208804 |   33427   16008   381268    23.8 | 82.643 % |
c |     23064 |  100121   208421 |   36769   16005   381628    23.8 | 82.869 % |
c |     23215 |   99847   207771 |   40446   16010   382609    23.9 | 83.086 % |
c |     23440 |   99378   206660 |   44491   15720   381098    24.2 | 83.466 % |
c |     23777 |   99378   206660 |   48940   16057   396983    24.7 | 83.466 % |
c |     24283 |   99055   205899 |   53834   16431   413707    25.2 | 83.714 % |
c |     25042 |   98743   205161 |   59217   16952   434576    25.6 | 83.960 % |
c |     26182 |   98687   205030 |   65139   18022   487887    27.1 | 84.001 % |
c |     27890 |   98568   204747 |   71653   19723   611342    31.0 | 84.098 % |
c ==============================================================================
c Found solution: -42
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28712 |   98520   204613 |   32840   20498   655584    32.0 | 84.098 % |
c |     28812 |   98520   204613 |   36124   20598   657760    31.9 | 84.116 % |
c |     28962 |   98178   203809 |   39736   20671   663998    32.1 | 84.379 % |
c |     29187 |   98178   203809 |   43710   20896   678393    32.5 | 84.379 % |
c |     29524 |   98098   203619 |   48081   21130   689415    32.6 | 84.441 % |
c |     30030 |   98092   203605 |   52889   21617   708609    32.8 | 84.445 % |
c |     30789 |   98092   203605 |   58178   22376   766634    34.3 | 84.445 % |
c |     31928 |   98074   203561 |   63995   23509   834097    35.5 | 84.463 % |
c |     33637 |   98068   203547 |   70395   25217  1102251    43.7 | 84.467 % |
c |     36199 |   98068   203547 |   77435   27779  1366929    49.2 | 84.467 % |
c |     40043 |   97606   202441 |   85178   31064  1669540    53.7 | 84.838 % |
c |     45811 |   97346   201835 |   93696   36633  2162577    59.0 | 85.027 % |
c |     54461 |   96576   200040 |  103065   45096  3420486    75.8 | 85.590 % |
c ==============================================================================
c Found solution: -43
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56932 |   96551   199998 |   32183   47467  3626738    76.4 | 85.590 % |
c |     57032 |   96551   199998 |   35401   47567  3628951    76.3 | 85.649 % |
c |     57182 |   96551   199998 |   38941   47717  3637251    76.2 | 85.649 % |
c |     57407 |   96551   199998 |   42835   47942  3655360    76.2 | 85.649 % |
c |     57744 |   96380   199599 |   47119   48044  3667051    76.3 | 85.774 % |
c |     58250 |   96376   199590 |   51831   48471  3697181    76.3 | 85.776 % |
c |     59009 |   96376   199590 |   57014   49230  3773639    76.7 | 85.776 % |
c |     60148 |   96077   198893 |   62715   49985  3868235    77.4 | 85.995 % |
c |     61856 |   94826   195955 |   68987   51501  4035066    78.3 | 86.961 % |
c |     64420 |   94806   195908 |   75885   54058  4214881    78.0 | 86.976 % |
c |     68265 |   94800   195894 |   83474   57899  4736524    81.8 | 86.980 % |
c |     74031 |   94792   195875 |   91821   63655  5359317    84.2 | 86.987 % |
c ==============================================================================
c Found solution: -44
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78975 |   94693   195627 |   31564   68474  6009661    87.8 | 86.987 % |
c |     79075 |   94693   195627 |   34720   68574  6013534    87.7 | 87.050 % |
c |     79225 |   94693   195627 |   38192   68724  6026168    87.7 | 87.050 % |
c |     79452 |   94693   195627 |   42011   68951  6044660    87.7 | 87.050 % |
c |     79790 |   94693   195627 |   46212   69289  6079681    87.7 | 87.050 % |
c |     80297 |   94693   195627 |   50834   69796  6109921    87.5 | 87.050 % |
c |     81057 |   94693   195627 |   55917   70556  6173268    87.5 | 87.050 % |
c |     82197 |   94685   195608 |   61509   71695  6283374    87.6 | 87.056 % |
c |     83906 |   94604   195415 |   67660   73222  6485369    88.6 | 87.123 % |
c |     86468 |   94604   195415 |   74426   75784  6817045    90.0 | 87.123 % |
c |     90312 |   94604   195415 |   81868   79628  7171945    90.1 | 87.123 % |
c |     96078 |   94604   195415 |   90055   85394  7850934    91.9 | 87.123 % |
c |    104727 |   94604   195415 |   99061   94043  8983016    95.5 | 87.123 % |
c |    117701 |   94524   195228 |  108967  106896 10663900    99.8 | 87.183 % |
c |    137163 |   94336   194785 |  119864  125770 13047197   103.7 | 87.330 % |
c |    166355 |   94326   194761 |  131850  154872 18193794   117.5 | 87.338 % |
c ==============================================================================
c Found solution: -45
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    196516 |   94375   194884 |   31458   28878  3553355   123.0 | 87.338 % |
c |    196616 |   94375   194884 |   34603   28978  3560527   122.9 | 87.316 % |
c |    196766 |   94375   194884 |   38064   29128  3563005   122.3 | 87.316 % |
c |    196991 |   94375   194884 |   41870   29353  3588058   122.2 | 87.316 % |
c |    197328 |   94375   194884 |   46057   29690  3609111   121.6 | 87.316 % |
c |    197834 |   93851   193669 |   50663   30173  3623411   120.1 | 87.692 % |
c |    198594 |   93821   193599 |   55729   30901  3688135   119.4 | 87.713 % |
c |    199733 |   93821   193599 |   61302   32040  3775753   117.8 | 87.713 % |
c |    201442 |   93809   193571 |   67433   33747  3902783   115.6 | 87.722 % |
c |    204004 |   93803   193557 |   74176   36306  4068171   112.1 | 87.726 % |
c |    207848 |   93701   193322 |   81593   40086  4401591   109.8 | 87.795 % |
c |    213614 |   92771   191133 |   89753   45666  4864349   106.5 | 88.511 % |
c |    222264 |   92771   191133 |   98728   54316  5832066   107.4 | 88.511 % |
c |    235238 |   92771   191133 |  108601   67290  7870669   117.0 | 88.511 % |
c ==============================================================================
c Found solution: -46
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    247782 |   92738   191028 |   30912   79474  9156513   115.2 | 88.511 % |
c |    247883 |   92738   191028 |   34003   20813  1427114    68.6 | 88.531 % |
c |    248033 |   92732   191014 |   37403   20961  1434156    68.4 | 88.535 % |
c |    248258 |   92722   190990 |   41143   21180  1445487    68.2 | 88.544 % |
c |    248596 |   92722   190990 |   45258   21518  1470992    68.4 | 88.544 % |
c |    249102 |   92722   190990 |   49784   22024  1515662    68.8 | 88.544 % |
c |    249862 |   92722   190990 |   54762   22784  1568915    68.9 | 88.544 % |
c |    251002 |   92722   190990 |   60238   23924  1646804    68.8 | 88.544 % |
c |    252711 |   92706   190953 |   66262   25618  1820844    71.1 | 88.554 % |
c |    255273 |   92566   190620 |   72888   28059  2041471    72.8 | 88.662 % |
c |    259117 |   92566   190620 |   80177   31903  2352459    73.7 | 88.662 % |
c |    264883 |   92566   190620 |   88195   37669  2927364    77.7 | 88.662 % |
c |    273533 |   92566   190620 |   97015   46319  4363175    94.2 | 88.662 % |
c |    286508 |   92358   190132 |  106716   59140  6191906   104.7 | 88.819 % |
c |    305969 |   92352   190118 |  117388   78598  8422171   107.2 | 88.823 % |
c |    335162 |   92352   190118 |  129127  107791 11281006   104.7 | 88.823 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -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 -C#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 19357
Raw data (stat): 19357 (runsolver) R 19356 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481825722 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5251 0 0 0 984 14 0 0 25 0 1 0 481825722 24252416 5229 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5921 5229 603 41 0 5880 0
vsize: 23684
[startup+20.002 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5255 0 0 0 1983 15 0 0 25 0 1 0 481825722 24252416 5233 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5921 5233 603 41 0 5880 0
vsize: 23684
[startup+30.0022 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5259 0 0 0 2982 15 0 0 25 0 1 0 481825722 24399872 5237 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5957 5237 603 41 0 5916 0
vsize: 23828
[startup+40.0027 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5261 0 0 0 3981 15 0 0 25 0 1 0 481825722 24399872 5239 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5957 5239 603 41 0 5916 0
vsize: 23828
[startup+50.0032 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5262 0 0 0 4981 15 0 0 25 0 1 0 481825722 24399872 5240 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5957 5240 603 41 0 5916 0
vsize: 23828
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5270 0 0 0 5981 15 0 0 25 0 1 0 481825722 24399872 5248 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5957 5248 603 41 0 5916 0
vsize: 23828
[startup+70.0041 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5271 0 0 0 6981 15 0 0 25 0 1 0 481825722 24399872 5249 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5957 5249 603 41 0 5916 0
vsize: 23828
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5549 0 0 0 7981 16 0 0 25 0 1 0 481825722 26341376 5527 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6431 5527 603 41 0 6390 0
vsize: 25724
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5553 0 0 0 8981 16 0 0 25 0 1 0 481825722 26341376 5531 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6431 5531 603 41 0 6390 0
vsize: 25724
[startup+100.033 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 5921 0 0 0 9983 17 0 0 25 0 1 0 481825722 27914240 5899 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6815 5899 603 41 0 6774 0
vsize: 27260
[startup+110.234 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 6481 0 0 0 11001 19 0 0 25 0 1 0 481825722 30269440 6459 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7390 6459 603 41 0 7349 0
vsize: 29560
[startup+120.235 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 7025 0 0 0 11999 21 0 0 25 0 1 0 481825722 32415744 7003 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7003 603 41 0 7873 0
vsize: 31656
[startup+130.236 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 7513 0 0 0 12998 22 0 0 25 0 1 0 481825722 34562048 7491 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8438 7491 603 41 0 8397 0
vsize: 33752
[startup+140.236 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 8047 0 0 0 13997 24 0 0 25 0 1 0 481825722 36712448 8025 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8963 8025 603 41 0 8922 0
vsize: 35852
[startup+150.236 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 8696 0 0 0 14995 25 0 0 25 0 1 0 481825722 39403520 8674 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9620 8674 603 41 0 9579 0
vsize: 38480
[startup+160.237 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 9132 0 0 0 15994 27 0 0 25 0 1 0 481825722 41148416 9110 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10046 9110 603 41 0 10005 0
vsize: 40184
[startup+170.238 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 9453 0 0 0 16993 28 0 0 25 0 1 0 481825722 42418176 9431 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10356 9431 603 41 0 10315 0
vsize: 41424
[startup+180.238 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 9819 0 0 0 17992 29 0 0 25 0 1 0 481825722 43896832 9797 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10717 9797 603 41 0 10676 0
vsize: 42868
[startup+190.239 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 10289 0 0 0 18991 31 0 0 25 0 1 0 481825722 45772800 10267 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11175 10267 603 41 0 11134 0
vsize: 44700
[startup+200.238 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 10737 0 0 0 19989 33 0 0 25 0 1 0 481825722 47640576 10715 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11631 10715 603 41 0 11590 0
vsize: 46524
[startup+210.238 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 11174 0 0 0 20988 34 0 0 25 0 1 0 481825722 49381376 11152 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12056 11152 603 41 0 12015 0
vsize: 48224
[startup+220.238 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 11606 0 0 0 21987 35 0 0 25 0 1 0 481825722 51507200 11584 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12575 11584 603 41 0 12534 0
vsize: 50300
[startup+230.237 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 11956 0 0 0 22986 36 0 0 25 0 1 0 481825722 52838400 11934 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12900 11934 603 41 0 12859 0
vsize: 51600
[startup+240.237 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 12302 0 0 0 23986 37 0 0 25 0 1 0 481825722 54312960 12280 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13260 12280 603 41 0 13219 0
vsize: 53040
[startup+250.237 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 12692 0 0 0 24985 37 0 0 25 0 1 0 481825722 55922688 12670 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 12670 603 41 0 13612 0
vsize: 54612
[startup+260.238 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 13028 0 0 0 25984 38 0 0 25 0 1 0 481825722 57253888 13006 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13978 13006 603 41 0 13937 0
vsize: 55912
[startup+270.238 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 13377 0 0 0 26984 39 0 0 25 0 1 0 481825722 58576896 13355 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14301 13355 603 41 0 14260 0
vsize: 57204
[startup+280.238 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 13707 0 0 0 27983 40 0 0 25 0 1 0 481825722 60035072 13685 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14657 13685 603 41 0 14616 0
vsize: 58628
[startup+290.238 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 14042 0 0 0 28982 41 0 0 25 0 1 0 481825722 61374464 14020 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14984 14020 603 41 0 14943 0
vsize: 59936
[startup+300.238 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 14456 0 0 0 29981 42 0 0 25 0 1 0 481825722 62980096 14434 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15376 14434 603 41 0 15335 0
vsize: 61504
[startup+310.238 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 14857 0 0 0 30980 43 0 0 25 0 1 0 481825722 64704512 14835 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15797 14835 603 41 0 15756 0
vsize: 63188
[startup+320.239 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 15190 0 0 0 31980 44 0 0 25 0 1 0 481825722 66043904 15168 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16124 15168 603 41 0 16083 0
vsize: 64496
[startup+330.238 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 15499 0 0 0 32979 45 0 0 25 0 1 0 481825722 67239936 15477 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16416 15477 603 41 0 16375 0
vsize: 65664
[startup+340.239 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 15805 0 0 0 33977 47 0 0 25 0 1 0 481825722 68575232 15783 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16742 15783 603 41 0 16701 0
vsize: 66968
[startup+350.238 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 16138 0 0 0 34976 48 0 0 25 0 1 0 481825722 69922816 16116 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17071 16116 603 41 0 17030 0
vsize: 68284
[startup+360.239 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 16560 0 0 0 35975 49 0 0 25 0 1 0 481825722 71532544 16538 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17464 16538 603 41 0 17423 0
vsize: 69856
[startup+370.239 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 16889 0 0 0 36974 51 0 0 25 0 1 0 481825722 72871936 16867 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17791 16867 603 41 0 17750 0
vsize: 71164
[startup+380.238 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 17121 0 0 0 37973 51 0 0 25 0 1 0 481825722 73814016 17099 4294967295 134512640 134672761 3221224560 3221223664 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18021 17099 603 41 0 17980 0
vsize: 72084
[startup+390.239 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 17403 0 0 0 38972 52 0 0 25 0 1 0 481825722 75014144 17381 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18314 17381 603 41 0 18273 0
vsize: 73256
[startup+400.24 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 17690 0 0 0 39972 53 0 0 25 0 1 0 481825722 76210176 17668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18606 17668 603 41 0 18565 0
vsize: 74424
[startup+410.24 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 17959 0 0 0 40971 54 0 0 25 0 1 0 481825722 77275136 17937 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18866 17937 603 41 0 18825 0
vsize: 75464
[startup+420.24 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 18246 0 0 0 41971 55 0 0 25 0 1 0 481825722 78483456 18224 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19161 18224 603 41 0 19120 0
vsize: 76644
[startup+430.24 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 18579 0 0 0 42969 56 0 0 25 0 1 0 481825722 79810560 18557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19485 18557 603 41 0 19444 0
vsize: 77940
[startup+440.24 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 18896 0 0 0 43969 57 0 0 25 0 1 0 481825722 81141760 18874 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19810 18874 603 41 0 19769 0
vsize: 79240
[startup+450.24 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 19224 0 0 0 44968 58 0 0 25 0 1 0 481825722 82477056 19202 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20136 19202 603 41 0 20095 0
vsize: 80544
[startup+460.241 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 19599 0 0 0 45967 59 0 0 25 0 1 0 481825722 83947520 19577 4294967295 134512640 134672761 3221224560 3221223664 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20495 19577 603 41 0 20454 0
vsize: 81980
[startup+470.242 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 19995 0 0 0 46967 60 0 0 25 0 1 0 481825722 85544960 19973 4294967295 134512640 134672761 3221224560 3221223664 134559784 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20885 19973 603 41 0 20844 0
vsize: 83540
[startup+480.241 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 20365 0 0 0 47966 61 0 0 25 0 1 0 481825722 87654400 20343 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21400 20343 603 41 0 21359 0
vsize: 85600
[startup+490.243 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 20702 0 0 0 48965 62 0 0 25 0 1 0 481825722 88981504 20680 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21724 20680 603 41 0 21683 0
vsize: 86896
[startup+500.242 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 21033 0 0 0 49964 63 0 0 25 0 1 0 481825722 90316800 21011 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22050 21011 603 41 0 22009 0
vsize: 88200
[startup+510.243 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 21335 0 0 0 50963 64 0 0 25 0 1 0 481825722 91516928 21313 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22343 21313 603 41 0 22302 0
vsize: 89372
[startup+520.243 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 21650 0 0 0 51963 65 0 0 25 0 1 0 481825722 92852224 21628 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22669 21628 603 41 0 22628 0
vsize: 90676
[startup+530.243 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 21931 0 0 0 52963 65 0 0 25 0 1 0 481825722 93925376 21909 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22931 21909 603 41 0 22890 0
vsize: 91724
[startup+540.243 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 22307 0 0 0 53961 66 0 0 25 0 1 0 481825722 95518720 22285 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23320 22285 603 41 0 23279 0
vsize: 93280
[startup+550.243 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 22644 0 0 0 54961 67 0 0 25 0 1 0 481825722 96858112 22622 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23647 22622 603 41 0 23606 0
vsize: 94588
[startup+560.244 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 22970 0 0 0 55960 68 0 0 25 0 1 0 481825722 98193408 22948 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23973 22948 603 41 0 23932 0
vsize: 95892
[startup+570.244 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 23252 0 0 0 56960 68 0 0 25 0 1 0 481825722 99397632 23230 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24267 23230 603 41 0 24226 0
vsize: 97068
[startup+580.244 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 23522 0 0 0 57959 69 0 0 25 0 1 0 481825722 100458496 23500 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24526 23500 603 41 0 24485 0
vsize: 98104
[startup+590.244 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 23759 0 0 0 58959 70 0 0 25 0 1 0 481825722 101392384 23737 4294967295 134512640 134672761 3221224560 3221223664 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24754 23737 603 41 0 24713 0
vsize: 99016
[startup+600.244 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 24027 0 0 0 59959 70 0 0 25 0 1 0 481825722 102588416 24005 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25046 24005 603 41 0 25005 0
vsize: 100184
[startup+610.245 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 24281 0 0 0 60958 71 0 0 25 0 1 0 481825722 103522304 24259 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25274 24259 603 41 0 25233 0
vsize: 101096
[startup+620.246 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 24545 0 0 0 61957 71 0 0 25 0 1 0 481825722 104583168 24523 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25533 24523 603 41 0 25492 0
vsize: 102132
[startup+630.245 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 24809 0 0 0 62956 72 0 0 25 0 1 0 481825722 105660416 24787 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25796 24787 603 41 0 25755 0
vsize: 103184
[startup+640.246 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 25093 0 0 0 63956 73 0 0 25 0 1 0 481825722 106860544 25071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26089 25071 603 41 0 26048 0
vsize: 104356
[startup+650.245 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 25355 0 0 0 64955 74 0 0 25 0 1 0 481825722 107917312 25333 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26347 25333 603 41 0 26306 0
vsize: 105388
[startup+660.246 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 25600 0 0 0 65955 74 0 0 25 0 1 0 481825722 108982272 25578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26607 25578 603 41 0 26566 0
vsize: 106428
[startup+670.247 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 25863 0 0 0 66955 75 0 0 25 0 1 0 481825722 110047232 25841 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26867 25841 603 41 0 26826 0
vsize: 107468
[startup+680.246 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 26133 0 0 0 67954 75 0 0 25 0 1 0 481825722 111108096 26111 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27126 26111 603 41 0 27085 0
vsize: 108504
[startup+690.246 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 26407 0 0 0 68954 76 0 0 25 0 1 0 481825722 112164864 26385 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27384 26385 603 41 0 27343 0
vsize: 109536
[startup+700.247 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 26681 0 0 0 69953 77 0 0 25 0 1 0 481825722 113373184 26659 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27679 26659 603 41 0 27638 0
vsize: 110716
[startup+710.247 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 26967 0 0 0 70952 78 0 0 25 0 1 0 481825722 114438144 26945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27939 26945 603 41 0 27898 0
vsize: 111756
[startup+720.247 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27274 0 0 0 71952 78 0 0 25 0 1 0 481825722 115761152 27252 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28262 27252 603 41 0 28221 0
vsize: 113048
[startup+730.247 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 19357
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27553 0 0 0 72951 79 0 0 25 0 1 0 481825722 116826112 27531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28522 27531 603 41 0 28481 0
vsize: 114088
[startup+740.247 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 19358
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27749 0 0 0 73950 80 0 0 25 0 1 0 481825722 117751808 27727 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28748 27727 603 41 0 28707 0
vsize: 114992
[startup+750.247 s]
Raw data (loadavg): 1.07 0.99 0.92 2/58 19400
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 74949 81 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223296 134565845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+760.375 s]
Raw data (loadavg): 1.21 1.02 0.93 2/54 19410
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 75962 81 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+770.376 s]
Raw data (loadavg): 1.18 1.02 0.93 2/54 19410
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 76962 81 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+780.376 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 19410
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 77962 81 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+790.376 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 19410
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 78962 81 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+800.377 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 19410
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 79962 81 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+810.378 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 19410
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 80963 81 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+820.378 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 19410
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 81963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+830.378 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 82963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+840.378 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 83963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+850.378 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 84963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+860.379 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 85963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+870.379 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 86963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+880.379 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 87963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+890.379 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 88963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223744 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+900.379 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 89963 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223744 134559392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+910.38 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 90964 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+920.381 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 91964 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+930.38 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 92964 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+940.381 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 93964 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+950.381 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 94964 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+960.382 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 95964 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+970.382 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 96964 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223560 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+980.381 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 97965 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+990.381 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 98965 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1000.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 99965 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1010.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 100965 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1020.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 101965 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1030.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 102965 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1040.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 103966 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223712 134565212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1050.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 104966 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1060.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 105966 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1070.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 106966 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223736 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1080.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19412
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 107966 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1090.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 108966 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1100.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 109967 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1110.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 110967 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1120.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 111967 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1130.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 112967 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1140.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 113967 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1150.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 114968 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1160.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 115968 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1170.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 116968 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1180.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 117968 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1190.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 118968 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
[startup+1200.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19414
Raw data (stat): 19357 (minisat+) R 19356 11931 11930 0 -1 0 27984 0 0 0 119968 82 0 0 25 0 1 0 481825722 118677504 27962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28974 27962 603 41 0 28933 0
vsize: 115896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.45 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 19414
Raw data (stat): 19357 (minisat+) Z 19356 11931 11930 0 -1 12 27987 0 0 0 119969 88 0 0 25 0 1 0 481825722 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.45
CPU time (s): 1200.57
CPU user time (s): 1199.69
CPU system time (s): 0.882865
CPU usage (%): 100.011
Max. virtual memory (Kb): 115896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####