PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb59-26-opb/normalized-frb59-26-2.opb
MD5SUM	5b8ef604a7452dcb7c7d749b75aed566
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-45
Optimality of the best value was proved	NO
Number of terms in the objective function	1534
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	1534
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	1534
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.15
Number of variables	1534
Total number of constraints	126163
Number of constraints which are clauses	126163
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5647

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 01:10:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4110 boxname=wulflinc32 idbench=350 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5b8ef604a7452dcb7c7d749b75aed566  /oldhome/oroussel/tmp/wulflinc32/normalized-frb59-26-2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc32/normalized-frb59-26-2.opb /oldhome/oroussel/tmp/wulflinc32/normalized-frb59-26-2.opb
IDLAUNCH: 4110
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034724 kB
MemFree:        702108 kB
Buffers:         35028 kB
Cached:         185508 kB
SwapCached:       1212 kB
Active:         149128 kB
Inactive:       151780 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        701852 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2316 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25932 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:31:02 (client local time) WITH STATUS 10 IN 1210.09 SECONDS
stats: 4110 7 1210.09 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 126163 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  126163   252326 |   37848       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |  126163   252326 |   50465       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 7.68283 s)
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:85954     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  216908   465199 |   65072       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/61774          
c   -- var.elim.:  2000/61774          
c   -- var.elim.:  3000/61774          
c   -- var.elim.:  4000/61774          
c   -- var.elim.:  5000/61774          
c   -- var.elim.:  6000/61774          
c   -- var.elim.:  7000/61774          
c   -- var.elim.:  8000/61774          
c   -- var.elim.:  9000/61774          
c   -- var.elim.:  10000/61774          
c   -- var.elim.:  11000/61774          
c   -- var.elim.:  12000/61774          
c   -- var.elim.:  13000/61774          
c   -- var.elim.:  14000/61774          
c   -- var.elim.:  15000/61774          
c   -- var.elim.:  16000/61774          
c   -- var.elim.:  17000/61774          
c   -- var.elim.:  18000/61774          
c   -- var.elim.:  19000/61774          
c   -- var.elim.:  20000/61774          
c   -- var.elim.:  21000/61774          
c   -- var.elim.:  22000/61774          
c   -- var.elim.:  23000/61774          
c   -- var.elim.:  24000/61774          
c   -- var.elim.:  25000/61774          
c   -- var.elim.:  26000/61774          
c   -- var.elim.:  27000/61774          
c   -- var.elim.:  28000/61774          
c   -- var.elim.:  29000/61774          
c   -- var.elim.:  30000/61774          
c   -- var.elim.:  31000/61774          
c   -- var.elim.:  32000/61774          
c   -- var.elim.:  33000/61774          
c   -- var.elim.:  34000/61774          
c   -- var.elim.:  35000/61774          
c   -- var.elim.:  36000/61774          
c   -- var.elim.:  37000/61774          
c   -- var.elim.:  38000/61774          
c   -- var.elim.:  39000/61774          
c   -- var.elim.:  40000/61774          
c   -- var.elim.:  41000/61774          
c   -- var.elim.:  42000/61774          
c   -- var.elim.:  43000/61774          
c   -- var.elim.:  44000/61774          
c   -- var.elim.:  45000/61774          
c   -- var.elim.:  46000/61774          
c   -- var.elim.:  47000/61774          
c   -- var.elim.:  48000/61774          
c   -- var.elim.:  49000/61774          
c   -- var.elim.:  50000/61774          
c   -- var.elim.:  51000/61774          
c   -- var.elim.:  52000/61774          
c   -- var.elim.:  53000/61774          
c   -- var.elim.:  54000/61774          
c   -- var.elim.:  55000/61774          
c   -- var.elim.:  56000/61774          
c   -- var.elim.:  57000/61774          
c   -- var.elim.:  58000/61774          
c   -- var.elim.:  59000/61774          
c   -- var.elim.:  60000/61774          
c   -- var.elim.:  61000/61774          
c   -- var.elim.:  61774/61774          
c   -- var.elim.:  1000/31242          
c   -- var.elim.:  2000/31242          
c   -- var.elim.:  3000/31242          
c   -- var.elim.:  4000/31242          
c   -- var.elim.:  5000/31242          
c   -- var.elim.:  6000/31242          
c   -- var.elim.:  7000/31242          
c   -- var.elim.:  8000/31242          
c   -- var.elim.:  9000/31242          
c   -- var.elim.:  10000/31242          
c   -- var.elim.:  11000/31242          
c   -- var.elim.:  12000/31242          
c   -- var.elim.:  13000/31242          
c   -- var.elim.:  14000/31242          
c   -- var.elim.:  15000/31242          
c   -- var.elim.:  16000/31242          
c   -- var.elim.:  17000/31242          
c   -- var.elim.:  18000/31242          
c   -- var.elim.:  19000/31242          
c   -- var.elim.:  20000/31242          
c   -- var.elim.:  21000/31242          
c   -- var.elim.:  22000/31242          
c   -- var.elim.:  23000/31242          
c   -- var.elim.:  24000/31242          
c   -- var.elim.:  25000/31242          
c   -- var.elim.:  26000/31242          
c   -- var.elim.:  27000/31242          
c   -- var.elim.:  28000/31242          
c   -- var.elim.:  29000/31242          
c   -- var.elim.:  30000/31242          
c   -- var.elim.:  31000/31242          
c   -- var.elim.:  31242/31242          
c   -- var.elim.:  1000/5766          
c   -- var.elim.:  2000/5766          
c   -- var.elim.:  3000/5766          
c   -- var.elim.:  4000/5766          
c   -- var.elim.:  5000/5766          
c   -- var.elim.:  5766/5766          
c   -- var.elim.:  94/94          
c   -- subsuming                       
c   -- var.elim.:  1000/11700          
c   -- var.elim.:  2000/11700          
c   -- var.elim.:  3000/11700          
c   -- var.elim.:  4000/11700          
c   -- var.elim.:  5000/11700          
c   -- var.elim.:  6000/11700          
c   -- var.elim.:  7000/11700          
c   -- var.elim.:  8000/11700          
c   -- var.elim.:  9000/11700          
c   -- var.elim.:  10000/11700          
c   -- var.elim.:  11000/11700          
c   -- var.elim.:  11700/11700          
c   -- var.elim.:  171/171          
c |         0 |  150832   473950 |      --       0       --      -- |     --   | -66070/8769
c |         0 |  150832   473950 |   60332       0        0     nan |  0.000 % |
c |       100 |  150832   473950 |   66366     100     9700    97.0 | 56.190 % |
c |       250 |  150832   473950 |   73002     250    35766   143.1 | 56.190 % |
c |       475 |  150832   473950 |   80302     475    80931   170.4 | 56.190 % |
c |       812 |  150832   473950 |   88333     812   162093   199.6 | 56.190 % |
c |      1318 |  150816   473761 |   97156    1315   269998   205.3 | 56.215 % |
c |      2077 |  150816   473761 |  106871    2074   416902   201.0 | 56.215 % |
c |      3216 |  150770   473313 |  117523    3208   659005   205.4 | 56.289 % |
c |      4924 |  150746   473082 |  129254    4914  1077382   219.2 | 56.328 % |
c |      7486 |  150716   472735 |  142152    7470  1719055   230.1 | 56.376 % |
c |     11330 |  150716   472735 |  156367   11314  2736308   241.9 | 56.376 % |
c |     17096 |  150434   470109 |  171682   17046  4569083   268.0 | 56.829 % |
c ==============================================================================
c (current CPU-time: 384.58 s)
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17364 |  157620   489325 |   47285   17314  4732177   273.3 | 56.829 % |
c   -- subsuming                       
c   -- var.elim.:  1000/17205          
c   -- var.elim.:  2000/17205          
c   -- var.elim.:  3000/17205          
c   -- var.elim.:  4000/17205          
c   -- var.elim.:  5000/17205          
c   -- var.elim.:  6000/17205          
c   -- var.elim.:  7000/17205          
c   -- var.elim.:  8000/17205          
c   -- var.elim.:  9000/17205          
c   -- var.elim.:  10000/17205          
c   -- var.elim.:  11000/17205          
c   -- var.elim.:  12000/17205          
c   -- var.elim.:  13000/17205          
c   -- var.elim.:  14000/17205          
c   -- var.elim.:  15000/17205          
c   -- var.elim.:  16000/17205          
c   -- var.elim.:  17000/17205          
c   -- var.elim.:  17205/17205          
c   -- var.elim.:  1000/4925          
c   -- var.elim.:  2000/4925          
c   -- var.elim.:  3000/4925          
c   -- var.elim.:  4000/4925          
c   -- var.elim.:  4925/4925          
c   -- var.elim.:  111/111          
c   -- var.elim.:  41/41          
c   -- subsuming                       
c   -- var.elim.:  1000/4661          
c   -- var.elim.:  2000/4661          
c   -- var.elim.:  3000/4661          
c   -- var.elim.:  4000/4661          
c   -- var.elim.:  4661/4661          
c   -- var.elim.:  56/56          
c |     17364 |  150586   478675 |      --   17314       --      -- |     --   | -7018/-10617
c |     17364 |  150586   478675 |   60234   17270  4716765   273.1 | 56.829 % |
c |     17465 |  150586   478675 |   66257   17371  4758870   274.0 | 60.387 % |
c |     17616 |  150586   478675 |   72883   17522  4775616   272.5 | 60.387 % |
c |     17841 |  150586   478675 |   80171   17747  4837170   272.6 | 60.387 % |
c |     18178 |  150586   478675 |   88189   18084  4907023   271.3 | 60.387 % |
c |     18684 |  150586   478675 |   97008   18590  5054983   271.9 | 60.387 % |
c |     19443 |  150564   478442 |  106693   19344  5290393   273.5 | 60.420 % |
c |     20582 |  150528   478131 |  117334   20477  5652496   276.0 | 60.472 % |
c |     22290 |  150346   476389 |  128912   22165  6174755   278.6 | 60.740 % |
c |     24852 |  150190   475009 |  141656   24694  7081570   286.8 | 60.969 % |
c |     28696 |  150094   474082 |  155722   28517  8342063   292.5 | 61.110 % |
c |     34462 |  149464   468346 |  170575   34194 10563462   308.9 | 62.035 % |
c |     43111 |  148388   458221 |  186282   42631 13667743   320.6 | 63.601 % |
c |     56085 |  147554   450029 |  203758   55413 18855876   340.3 | 64.815 % |
c ==============================================================================
c (current CPU-time: 829.037 s)
c ==============================================================================
c [1mFound solution: -46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     66422 |  147110   443661 |   44132   65513 23444391   357.9 | 64.815 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10248          
c   -- var.elim.:  2000/10248          
c   -- var.elim.:  3000/10248          
c   -- var.elim.:  4000/10248          
c   -- var.elim.:  5000/10248          
c   -- var.elim.:  6000/10248          
c   -- var.elim.:  7000/10248          
c   -- var.elim.:  8000/10248          
c   -- var.elim.:  9000/10248          
c   -- var.elim.:  10000/10248          
c   -- var.elim.:  10248/10248          
c   -- var.elim.:  451/451          
c   -- subsuming                       
c   -- var.elim.:  134/134          
c |     66422 |  146858   437869 |      --   65513       --      -- |     --   | -234/-768
c |     66422 |  146858   437869 |   58743   59008 14198078   240.6 | 64.815 % |
c |     66523 |  146688   436218 |   64542   59102 14215325   240.5 | 66.174 % |
c |     66673 |  146658   435926 |   70982   59222 14263462   240.8 | 66.215 % |
c |     66898 |  146658   435926 |   78080   59447 14318809   240.9 | 66.215 % |
c |     67237 |  146601   435355 |   85855   59784 14388927   240.7 | 66.294 % |
c |     67743 |  146565   434960 |   94417   60270 14562030   241.6 | 66.347 % |
c |     68502 |  146515   434506 |  103824   61022 14866144   243.6 | 66.421 % |
c |     69642 |  146428   433661 |  114138   62124 15358751   247.2 | 66.544 % |
c |     71350 |  146338   432715 |  125475   63801 15952187   250.0 | 66.674 % |
c |     73912 |  146270   432087 |  137958   66349 16902801   254.8 | 66.774 % |
c |     77757 |  146129   430675 |  151608   70138 18502606   263.8 | 66.973 % |
c |     83523 |  145857   428142 |  166458   75844 20557778   271.1 | 67.364 % |
c |     92172 |  145625   425841 |  182813   84439 24773606   293.4 | 67.687 % |
c |    105146 |  145318   422894 |  200670   97271 30371614   312.2 | 68.137 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1534 C1533 -C1532 -C1531 -C1530 -C1529 -C1528 -C1527 -C1526 -C1525 -C1524 -C1523 -C1522 -C1521 -C1520 -C1519 -C1518 -C1517 -C1516 -C1515 -C1514 -C1513 -C1512 -C1511 -C1510 -C1509 -C1508 -C1507 -C1506 -C1505 -C1504 -C1503 -C1502 -C1501 -C1500 -C1499 -C1498 -C1497 -C1496 -C1495 -C1494 -C1493 -C1492 -C1491 -C1490 -C1489 -C1488 -C1487 -C1486 -C1485 -C1484 -C1483 -C1482 -C1481 -C1480 -C1479 -C1478 -C1477 -C1476 -C1475 -C1474 C1473 -C1472 -C1471 -C1470 -C1469 -C1468 -C1467 -C1466 -C1465 -C1464 -C1463 -C1462 -C1461 -C1460 -C1459 -C1458 -C1457 -C1456 -C1455 C1454 -C1453 -C1452 -C1451 -C1450 -C1449 -C1448 -C1447 -C1446 -C1445 -C1444 -C1443 -C1442 -C1441 -C1440 -C1439 -C1438 -C1437 -C1436 -C1435 -C1434 -C1433 -C1432 -C1431 -C1430 -C1429 -C1428 -C1427 -C1426 -C1425 -C1424 -C1423 -C1422 -C1421 -C1420 -C1419 -C1418 C1417 -C1416 -C1415 -C1414 -C1413 -C1412 -C1411 -C1410 -C1409 -C1408 -C1407 -C1406 -C1405 -C1404 -C1403 -C1402 -C1401 -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 -C1386 -C1385 -C1384 -C1383 -C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 -C1361 -C1360 -C1359 -C1358 -C1357 -C1356 C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 -C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 C1281 -C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 -C1273 -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -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 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 #### 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.93 0.98 0.91 2/53 13943
Raw data (stat): 13943 (runsolver) R 13942 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480522018 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.94 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 11986 0 0 0 967 31 0 0 25 0 1 0 480522018 49008640 11136 4294967295 134512640 134672761 3221224560 3221222736 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11965 11136 603 41 0 11924 0
vsize: 47860
[startup+20.0032 s]
Raw data (loadavg): 0.95 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12928 0 0 0 1943 54 0 0 25 0 1 0 480522018 52924416 12078 4294967295 134512640 134672761 3221224560 3221222144 134566484 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12921 12078 603 41 0 12880 0
vsize: 51684
[startup+30.004 s]
Raw data (loadavg): 0.95 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12942 0 0 0 2943 54 0 0 25 0 1 0 480522018 53010432 12092 4294967295 134512640 134672761 3221224560 3221222992 134605453 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12942 12092 603 41 0 12901 0
vsize: 51768
[startup+40.0047 s]
Raw data (loadavg): 0.96 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12975 0 0 0 3944 54 0 0 25 0 1 0 480522018 53272576 12125 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12125 603 41 0 12965 0
vsize: 52024
[startup+50.0056 s]
Raw data (loadavg): 0.97 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12976 0 0 0 4944 54 0 0 25 0 1 0 480522018 53272576 12126 4294967295 134512640 134672761 3221224560 3221222992 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12126 603 41 0 12965 0
vsize: 52024
[startup+60.0073 s]
Raw data (loadavg): 0.97 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12977 0 0 0 5944 54 0 0 25 0 1 0 480522018 53272576 12127 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12127 603 41 0 12965 0
vsize: 52024
[startup+70.0078 s]
Raw data (loadavg): 0.97 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12978 0 0 0 6944 54 0 0 25 0 1 0 480522018 53272576 12128 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12128 603 41 0 12965 0
vsize: 52024
[startup+80.0088 s]
Raw data (loadavg): 0.98 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12979 0 0 0 7945 54 0 0 25 0 1 0 480522018 53272576 12129 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12129 603 41 0 12965 0
vsize: 52024
[startup+90.0096 s]
Raw data (loadavg): 0.98 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12981 0 0 0 8945 54 0 0 25 0 1 0 480522018 53272576 12131 4294967295 134512640 134672761 3221224560 3221222992 134604064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12131 603 41 0 12965 0
vsize: 52024
[startup+100.01 s]
Raw data (loadavg): 0.98 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12982 0 0 0 9945 54 0 0 25 0 1 0 480522018 53272576 12132 4294967295 134512640 134672761 3221224560 3221222992 134604055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12132 603 41 0 12965 0
vsize: 52024
[startup+110.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12983 0 0 0 10945 54 0 0 25 0 1 0 480522018 53272576 12133 4294967295 134512640 134672761 3221224560 3221223008 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12133 603 41 0 12965 0
vsize: 52024
[startup+120.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12985 0 0 0 11945 54 0 0 25 0 1 0 480522018 53272576 12135 4294967295 134512640 134672761 3221224560 3221222224 134566712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12135 603 41 0 12965 0
vsize: 52024
[startup+130.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12986 0 0 0 12946 54 0 0 25 0 1 0 480522018 53272576 12136 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12136 603 41 0 12965 0
vsize: 52024
[startup+140.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 12991 0 0 0 13946 54 0 0 25 0 1 0 480522018 53272576 12141 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12141 603 41 0 12965 0
vsize: 52024
[startup+150.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13002 0 0 0 14946 54 0 0 25 0 1 0 480522018 53272576 12152 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12152 603 41 0 12965 0
vsize: 52024
[startup+160.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13023 0 0 0 15946 54 0 0 25 0 1 0 480522018 53534720 12173 4294967295 134512640 134672761 3221224560 3221222656 134566548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12173 603 41 0 13029 0
vsize: 52280
[startup+170.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13027 0 0 0 16946 54 0 0 25 0 1 0 480522018 53534720 12177 4294967295 134512640 134672761 3221224560 3221222992 134605448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12177 603 41 0 13029 0
vsize: 52280
[startup+180.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13031 0 0 0 17947 54 0 0 25 0 1 0 480522018 53534720 12181 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12181 603 41 0 13029 0
vsize: 52280
[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13035 0 0 0 18947 54 0 0 25 0 1 0 480522018 53534720 12185 4294967295 134512640 134672761 3221224560 3221223152 134607812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12185 603 41 0 13029 0
vsize: 52280
[startup+200.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13039 0 0 0 19947 54 0 0 25 0 1 0 480522018 53534720 12189 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12189 603 41 0 13029 0
vsize: 52280
[startup+210.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13045 0 0 0 20948 54 0 0 25 0 1 0 480522018 53534720 12195 4294967295 134512640 134672761 3221224560 3221222992 134604055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12195 603 41 0 13029 0
vsize: 52280
[startup+220.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13051 0 0 0 21948 54 0 0 25 0 1 0 480522018 53534720 12201 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12201 603 41 0 13029 0
vsize: 52280
[startup+230.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13087 0 0 0 22948 55 0 0 25 0 1 0 480522018 53547008 12176 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 12176 603 41 0 13032 0
vsize: 52292
[startup+240.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13087 0 0 0 23948 55 0 0 25 0 1 0 480522018 53547008 12176 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 12176 603 41 0 13032 0
vsize: 52292
[startup+250.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13087 0 0 0 24947 55 0 0 25 0 1 0 480522018 53547008 12176 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 12176 603 41 0 13032 0
vsize: 52292
[startup+260.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13087 0 0 0 25947 55 0 0 25 0 1 0 480522018 53547008 12176 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 12176 603 41 0 13032 0
vsize: 52292
[startup+270.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13527 0 0 0 26947 56 0 0 25 0 1 0 480522018 55660544 12555 4294967295 134512640 134672761 3221224560 3221222960 134604621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13589 12555 603 41 0 13548 0
vsize: 54356
[startup+280.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13527 0 0 0 27947 56 0 0 25 0 1 0 480522018 55660544 12555 4294967295 134512640 134672761 3221224560 3221223056 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13589 12555 603 41 0 13548 0
vsize: 54356
[startup+290.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13527 0 0 0 28947 56 0 0 25 0 1 0 480522018 55660544 12555 4294967295 134512640 134672761 3221224560 3221223052 134642774 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13589 12555 603 41 0 13548 0
vsize: 54356
[startup+300.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13527 0 0 0 29947 56 0 0 25 0 1 0 480522018 55660544 12555 4294967295 134512640 134672761 3221224560 3221222960 134604075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13589 12555 603 41 0 13548 0
vsize: 54356
[startup+310.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13527 0 0 0 30947 57 0 0 25 0 1 0 480522018 53284864 12115 4294967295 134512640 134672761 3221224560 3221223008 134643532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13009 12115 603 41 0 12968 0
vsize: 52036
[startup+320.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13527 0 0 0 31947 57 0 0 25 0 1 0 480522018 53284864 12115 4294967295 134512640 134672761 3221224560 3221223008 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13009 12115 603 41 0 12968 0
vsize: 52036
[startup+330.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 13708 0 0 0 32947 57 0 0 25 0 1 0 480522018 54075392 12296 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13202 12296 603 41 0 13161 0
vsize: 52808
[startup+340.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 14278 0 0 0 33946 58 0 0 25 0 1 0 480522018 56336384 12866 4294967295 134512640 134672761 3221224560 3221223684 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13754 12866 603 41 0 13713 0
vsize: 55016
[startup+350.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 14986 0 0 0 34945 60 0 0 25 0 1 0 480522018 59252736 13574 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14466 13574 603 41 0 14425 0
vsize: 57864
[startup+360.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 15813 0 0 0 35944 61 0 0 25 0 1 0 480522018 62660608 14401 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15298 14401 603 41 0 15257 0
vsize: 61192
[startup+370.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 16543 0 0 0 36943 63 0 0 25 0 1 0 480522018 65662976 15131 4294967295 134512640 134672761 3221224560 3221223684 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16031 15131 603 41 0 15990 0
vsize: 64124
[startup+380.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 17270 0 0 0 37942 64 0 0 25 0 1 0 480522018 68681728 15858 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16768 15858 603 41 0 16727 0
vsize: 67072
[startup+390.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 20590 0 0 0 38927 78 0 0 25 0 1 0 480522018 81661952 17423 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19937 17423 603 41 0 19896 0
vsize: 79748
[startup+400.036 s]
Raw data (loadavg): 1.07 1.00 0.92 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 20590 0 0 0 39860 117 0 0 25 0 1 0 480522018 78200832 16999 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19092 16999 603 41 0 19051 0
vsize: 76368
[startup+410.036 s]
Raw data (loadavg): 1.14 1.02 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 20590 0 0 0 40860 118 0 0 25 0 1 0 480522018 78200832 16999 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19092 16999 603 41 0 19051 0
vsize: 76368
[startup+420.037 s]
Raw data (loadavg): 1.11 1.02 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 20590 0 0 0 41861 118 0 0 25 0 1 0 480522018 78200832 16999 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19092 16999 603 41 0 19051 0
vsize: 76368
[startup+430.038 s]
Raw data (loadavg): 1.10 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 21014 0 0 0 42860 119 0 0 25 0 1 0 480522018 81506304 17423 4294967295 134512640 134672761 3221224560 3221223272 134643442 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19899 17423 603 41 0 19858 0
vsize: 79596
[startup+440.038 s]
Raw data (loadavg): 1.08 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 21014 0 0 0 43859 119 0 0 25 0 1 0 480522018 81506304 17423 4294967295 134512640 134672761 3221224560 3221223104 134621227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19899 17423 603 41 0 19858 0
vsize: 79596
[startup+450.039 s]
Raw data (loadavg): 1.07 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 21014 0 0 0 44859 119 0 0 25 0 1 0 480522018 78200832 16999 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19092 16999 603 41 0 19051 0
vsize: 76368
[startup+460.04 s]
Raw data (loadavg): 1.06 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 21356 0 0 0 45859 120 0 0 25 0 1 0 480522018 79609856 17341 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19436 17341 603 41 0 19395 0
vsize: 77744
[startup+470.041 s]
Raw data (loadavg): 1.05 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 21934 0 0 0 46858 121 0 0 25 0 1 0 480522018 81969152 17919 4294967295 134512640 134672761 3221224560 3221223408 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20012 17919 603 41 0 19971 0
vsize: 80048
[startup+480.042 s]
Raw data (loadavg): 1.04 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 22493 0 0 0 47857 122 0 0 25 0 1 0 480522018 84312064 18478 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20584 18478 603 41 0 20543 0
vsize: 82336
[startup+490.043 s]
Raw data (loadavg): 1.03 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 23126 0 0 0 48856 123 0 0 25 0 1 0 480522018 86781952 19111 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21187 19111 603 41 0 21146 0
vsize: 84748
[startup+500.044 s]
Raw data (loadavg): 1.03 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 23809 0 0 0 49854 125 0 0 25 0 1 0 480522018 89616384 19794 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21879 19794 603 41 0 21838 0
vsize: 87516
[startup+510.045 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 24318 0 0 0 50853 127 0 0 25 0 1 0 480522018 91725824 20303 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22394 20303 603 41 0 22353 0
vsize: 89576
[startup+520.046 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 25195 0 0 0 51851 129 0 0 25 0 1 0 480522018 95305728 21180 4294967295 134512640 134672761 3221224560 3221223760 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23268 21180 603 41 0 23227 0
vsize: 93072
[startup+530.046 s]
Raw data (loadavg): 1.02 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 25526 0 0 0 52850 130 0 0 25 0 1 0 480522018 96616448 21511 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23588 21511 603 41 0 23547 0
vsize: 94352
[startup+540.047 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 26060 0 0 0 53849 131 0 0 25 0 1 0 480522018 98820096 22045 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24126 22045 603 41 0 24085 0
vsize: 96504
[startup+550.048 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 26396 0 0 0 54849 132 0 0 25 0 1 0 480522018 100384768 22381 4294967295 134512640 134672761 3221224560 3221223600 134614191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24508 22381 603 41 0 24467 0
vsize: 98032
[startup+560.048 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 26843 0 0 0 55848 133 0 0 25 0 1 0 480522018 102191104 22828 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24949 22828 603 41 0 24908 0
vsize: 99796
[startup+570.048 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 27201 0 0 0 56847 134 0 0 25 0 1 0 480522018 103604224 23186 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25294 23186 603 41 0 25253 0
vsize: 101176
[startup+580.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 27737 0 0 0 57847 135 0 0 25 0 1 0 480522018 105840640 23722 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25840 23722 603 41 0 25799 0
vsize: 103360
[startup+590.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 28239 0 0 0 58846 136 0 0 25 0 1 0 480522018 107900928 24224 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26343 24224 603 41 0 26302 0
vsize: 105372
[startup+600.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 28479 0 0 0 59846 136 0 0 25 0 1 0 480522018 108818432 24464 4294967295 134512640 134672761 3221224560 3221223136 134566562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26567 24464 603 41 0 26526 0
vsize: 106268
[startup+610.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 29284 0 0 0 60844 139 0 0 25 0 1 0 480522018 112177152 25269 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27387 25269 603 41 0 27346 0
vsize: 109548
[startup+620.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 29678 0 0 0 61843 140 0 0 25 0 1 0 480522018 113729536 25663 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27766 25663 603 41 0 27725 0
vsize: 111064
[startup+630.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 30098 0 0 0 62841 141 0 0 25 0 1 0 480522018 115392512 26083 4294967295 134512640 134672761 3221224560 3221223744 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28172 26083 603 41 0 28131 0
vsize: 112688
[startup+640.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 30479 0 0 0 63841 142 0 0 25 0 1 0 480522018 117059584 26464 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28579 26464 603 41 0 28538 0
vsize: 114316
[startup+650.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 30923 0 0 0 64839 144 0 0 25 0 1 0 480522018 118784000 26908 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29000 26908 603 41 0 28959 0
vsize: 116000
[startup+660.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 31359 0 0 0 65839 145 0 0 25 0 1 0 480522018 120639488 27344 4294967295 134512640 134672761 3221224560 3221223760 134610669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29453 27344 603 41 0 29412 0
vsize: 117812
[startup+670.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 31900 0 0 0 66837 146 0 0 25 0 1 0 480522018 122839040 27885 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29990 27885 603 41 0 29949 0
vsize: 119960
[startup+680.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 32221 0 0 0 67837 147 0 0 25 0 1 0 480522018 124162048 28206 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30313 28206 603 41 0 30272 0
vsize: 121252
[startup+690.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 32661 0 0 0 68836 148 0 0 25 0 1 0 480522018 125968384 28646 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30754 28646 603 41 0 30713 0
vsize: 123016
[startup+700.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 33210 0 0 0 69835 149 0 0 25 0 1 0 480522018 128180224 29195 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31294 29195 603 41 0 31253 0
vsize: 125176
[startup+710.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 33923 0 0 0 70833 151 0 0 25 0 1 0 480522018 131096576 29908 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32006 29908 603 41 0 31965 0
vsize: 128024
[startup+720.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 34438 0 0 0 71832 153 0 0 25 0 1 0 480522018 133115904 30423 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32499 30423 603 41 0 32458 0
vsize: 129996
[startup+730.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 34913 0 0 0 72831 154 0 0 25 0 1 0 480522018 135086080 30898 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32980 30898 603 41 0 32939 0
vsize: 131920
[startup+740.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 35471 0 0 0 73830 155 0 0 25 0 1 0 480522018 137363456 31456 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33536 31456 603 41 0 33495 0
vsize: 134144
[startup+750.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 35836 0 0 0 74830 156 0 0 25 0 1 0 480522018 138903552 31821 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33912 31821 603 41 0 33871 0
vsize: 135648
[startup+760.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 36321 0 0 0 75829 157 0 0 25 0 1 0 480522018 140820480 32306 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34380 32306 603 41 0 34339 0
vsize: 137520
[startup+770.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 36613 0 0 0 76829 157 0 0 25 0 1 0 480522018 142004224 32598 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34669 32598 603 41 0 34628 0
vsize: 138676
[startup+780.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 36878 0 0 0 77828 158 0 0 25 0 1 0 480522018 143167488 32863 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34953 32863 603 41 0 34912 0
vsize: 139812
[startup+790.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 37353 0 0 0 78828 159 0 0 25 0 1 0 480522018 145027072 33338 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35407 33338 603 41 0 35366 0
vsize: 141628
[startup+800.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 37940 0 0 0 79827 160 0 0 25 0 1 0 480522018 147460096 33925 4294967295 134512640 134672761 3221224560 3221223704 134616108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36001 33925 603 41 0 35960 0
vsize: 144004
[startup+810.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 38548 0 0 0 80826 161 0 0 25 0 1 0 480522018 149995520 34533 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36620 34533 603 41 0 36579 0
vsize: 146480
[startup+820.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 39028 0 0 0 81825 162 0 0 25 0 1 0 480522018 151932928 35013 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37093 35013 603 41 0 37052 0
vsize: 148372
[startup+830.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 39441 0 0 0 82824 163 0 0 25 0 1 0 480522018 153624576 35426 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37506 35426 603 41 0 37465 0
vsize: 150024
[startup+840.065 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42073 0 0 0 83806 181 0 0 25 0 1 0 480522018 158433280 36237 4294967295 134512640 134672761 3221224560 3221223104 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38680 36237 603 41 0 38639 0
vsize: 154720
[startup+850.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42073 0 0 0 84806 181 0 0 25 0 1 0 480522018 155107328 35813 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37868 35813 603 41 0 37827 0
vsize: 151472
[startup+860.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42496 0 0 0 85805 182 0 0 25 0 1 0 480522018 155107328 35813 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37868 35813 603 41 0 37827 0
vsize: 151472
[startup+870.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42496 0 0 0 86806 182 0 0 25 0 1 0 480522018 155107328 35813 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37868 35813 603 41 0 37827 0
vsize: 151472
[startup+880.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42496 0 0 0 87806 182 0 0 25 0 1 0 480522018 155107328 35813 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37868 35813 603 41 0 37827 0
vsize: 151472
[startup+890.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42496 0 0 0 88806 182 0 0 25 0 1 0 480522018 155107328 35813 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37868 35813 603 41 0 37827 0
vsize: 151472
[startup+900.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42496 0 0 0 89806 182 0 0 25 0 1 0 480522018 155107328 35813 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37868 35813 603 41 0 37827 0
vsize: 151472
[startup+910.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42496 0 0 0 90807 182 0 0 25 0 1 0 480522018 155107328 35813 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37868 35813 603 41 0 37827 0
vsize: 151472
[startup+920.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42497 0 0 0 91807 182 0 0 25 0 1 0 480522018 155369472 35814 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35814 603 41 0 37891 0
vsize: 151728
[startup+930.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42500 0 0 0 92807 182 0 0 25 0 1 0 480522018 155369472 35817 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35817 603 41 0 37891 0
vsize: 151728
[startup+940.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42501 0 0 0 93807 182 0 0 25 0 1 0 480522018 155369472 35818 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35818 603 41 0 37891 0
vsize: 151728
[startup+950.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42502 0 0 0 94808 182 0 0 25 0 1 0 480522018 155369472 35819 4294967295 134512640 134672761 3221224560 3221223744 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35819 603 41 0 37891 0
vsize: 151728
[startup+960.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42503 0 0 0 95808 182 0 0 25 0 1 0 480522018 155369472 35820 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35820 603 41 0 37891 0
vsize: 151728
[startup+970.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42504 0 0 0 96808 182 0 0 25 0 1 0 480522018 155369472 35821 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35821 603 41 0 37891 0
vsize: 151728
[startup+980.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42505 0 0 0 97808 182 0 0 25 0 1 0 480522018 155369472 35822 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35822 603 41 0 37891 0
vsize: 151728
[startup+990.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42506 0 0 0 98808 182 0 0 25 0 1 0 480522018 155369472 35823 4294967295 134512640 134672761 3221224560 3221223704 134616108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35823 603 41 0 37891 0
vsize: 151728
[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42507 0 0 0 99809 182 0 0 25 0 1 0 480522018 155369472 35824 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35824 603 41 0 37891 0
vsize: 151728
[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42508 0 0 0 100809 182 0 0 25 0 1 0 480522018 155369472 35825 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35825 603 41 0 37891 0
vsize: 151728
[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42509 0 0 0 101809 182 0 0 25 0 1 0 480522018 155369472 35826 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35826 603 41 0 37891 0
vsize: 151728
[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42511 0 0 0 102809 182 0 0 25 0 1 0 480522018 155369472 35828 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35828 603 41 0 37891 0
vsize: 151728
[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42512 0 0 0 103810 182 0 0 25 0 1 0 480522018 155369472 35829 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35829 603 41 0 37891 0
vsize: 151728
[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42513 0 0 0 104810 182 0 0 25 0 1 0 480522018 155369472 35830 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35830 603 41 0 37891 0
vsize: 151728
[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 42564 0 0 0 105810 182 0 0 25 0 1 0 480522018 155635712 35881 4294967295 134512640 134672761 3221224560 3221223704 134616126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37997 35881 603 41 0 37956 0
vsize: 151988
[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 43086 0 0 0 106809 184 0 0 25 0 1 0 480522018 157822976 36403 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38531 36403 603 41 0 38490 0
vsize: 154124
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 43752 0 0 0 107808 185 0 0 25 0 1 0 480522018 160559104 37069 4294967295 134512640 134672761 3221224560 3221223568 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39199 37069 603 41 0 39158 0
vsize: 156796
[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 44050 0 0 0 108807 186 0 0 25 0 1 0 480522018 161726464 37367 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39484 37367 603 41 0 39443 0
vsize: 157936
[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 44710 0 0 0 109806 188 0 0 25 0 1 0 480522018 164438016 38027 4294967295 134512640 134672761 3221224560 3221223704 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40146 38027 603 41 0 40105 0
vsize: 160584
[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 45205 0 0 0 110805 188 0 0 25 0 1 0 480522018 166375424 38522 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40619 38522 603 41 0 40578 0
vsize: 162476
[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 45585 0 0 0 111804 190 0 0 25 0 1 0 480522018 168030208 38902 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41023 38902 603 41 0 40982 0
vsize: 164092
[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 46044 0 0 0 112803 191 0 0 25 0 1 0 480522018 169861120 39361 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41470 39361 603 41 0 41429 0
vsize: 165880
[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 46612 0 0 0 113802 192 0 0 25 0 1 0 480522018 172187648 39929 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42038 39929 603 41 0 41997 0
vsize: 168152
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 47207 0 0 0 114800 194 0 0 25 0 1 0 480522018 174612480 40524 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42630 40524 603 41 0 42589 0
vsize: 170520
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 47677 0 0 0 115799 196 0 0 25 0 1 0 480522018 176582656 40994 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43111 40994 603 41 0 43070 0
vsize: 172444
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 48031 0 0 0 116798 197 0 0 25 0 1 0 480522018 178049024 41348 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43469 41348 603 41 0 43428 0
vsize: 173876
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 48397 0 0 0 117798 198 0 0 25 0 1 0 480522018 179527680 41714 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43830 41714 603 41 0 43789 0
vsize: 175320
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 48947 0 0 0 118797 199 0 0 25 0 1 0 480522018 181727232 42264 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44367 42264 603 41 0 44326 0
vsize: 177468
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 49219 0 0 0 119796 200 0 0 25 0 1 0 480522018 182878208 42536 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44648 42536 603 41 0 44607 0
vsize: 178592
[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 13943
Raw data (stat): 13943 (minisat+) R 13942 7987 7986 0 -1 0 49603 0 0 0 120795 201 0 0 25 0 1 0 480522018 184414208 42920 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45023 42920 603 41 0 44982 0
vsize: 180092
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.23 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 13943
Raw data (stat): 13943 (minisat+) Z 13942 7987 7986 0 -1 12 49604 0 0 0 120795 213 0 0 24 0 1 0 480522018 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): 1210.23
CPU time (s): 1210.09
CPU user time (s): 1207.96
CPU system time (s): 2.13168
CPU usage (%): 99.9884
Max. virtual memory (Kb): 180092
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####