PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb45-21-opb/normalized-frb45-21-1.opb
MD5SUM	aa1ea44fce5b7bfbe62733720f941ebb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-33
Optimality of the best value was proved	NO
Number of terms in the objective function	945
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	945
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	945
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	945
Total number of constraints	59186
Number of constraints which are clauses	59186
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 5622

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 00:57:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4089 boxname=wulflinc30 idbench=329 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  aa1ea44fce5b7bfbe62733720f941ebb  /oldhome/oroussel/tmp/wulflinc30/normalized-frb45-21-1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc30/normalized-frb45-21-1.opb /oldhome/oroussel/tmp/wulflinc30/normalized-frb45-21-1.opb
IDLAUNCH: 4089
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        732392 kB
Buffers:         37848 kB
Cached:         223340 kB
SwapCached:          0 kB
Active:          83408 kB
Inactive:       180660 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        732140 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32552 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:18:03 (client local time) WITH STATUS 10 IN 1209.73 SECONDS
stats: 4089 7 1209.73 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 59186 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 |   59186   118372 |   17755       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   59186   118372 |   23674       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 2.71659 s)
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  104775   225435 |   31432       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/31178          
c   -- var.elim.:  2000/31178          
c   -- var.elim.:  3000/31178          
c   -- var.elim.:  4000/31178          
c   -- var.elim.:  5000/31178          
c   -- var.elim.:  6000/31178          
c   -- var.elim.:  7000/31178          
c   -- var.elim.:  8000/31178          
c   -- var.elim.:  9000/31178          
c   -- var.elim.:  10000/31178          
c   -- var.elim.:  11000/31178          
c   -- var.elim.:  12000/31178          
c   -- var.elim.:  13000/31178          
c   -- var.elim.:  14000/31178          
c   -- var.elim.:  15000/31178          
c   -- var.elim.:  16000/31178          
c   -- var.elim.:  17000/31178          
c   -- var.elim.:  18000/31178          
c   -- var.elim.:  19000/31178          
c   -- var.elim.:  20000/31178          
c   -- var.elim.:  21000/31178          
c   -- var.elim.:  22000/31178          
c   -- var.elim.:  23000/31178          
c   -- var.elim.:  24000/31178          
c   -- var.elim.:  25000/31178          
c   -- var.elim.:  26000/31178          
c   -- var.elim.:  27000/31178          
c   -- var.elim.:  28000/31178          
c   -- var.elim.:  29000/31178          
c   -- var.elim.:  30000/31178          
c   -- var.elim.:  31000/31178          
c   -- var.elim.:  31178/31178          
c   -- var.elim.:  1000/15826          
c   -- var.elim.:  2000/15826          
c   -- var.elim.:  3000/15826          
c   -- var.elim.:  4000/15826          
c   -- var.elim.:  5000/15826          
c   -- var.elim.:  6000/15826          
c   -- var.elim.:  7000/15826          
c   -- var.elim.:  8000/15826          
c   -- var.elim.:  9000/15826          
c   -- var.elim.:  10000/15826          
c   -- var.elim.:  11000/15826          
c   -- var.elim.:  12000/15826          
c   -- var.elim.:  13000/15826          
c   -- var.elim.:  14000/15826          
c   -- var.elim.:  15000/15826          
c   -- var.elim.:  15826/15826          
c   -- var.elim.:  1000/3651          
c   -- var.elim.:  2000/3651          
c   -- var.elim.:  3000/3651          
c   -- var.elim.:  3651/3651          
c   -- subsuming                       
c   -- var.elim.:  1000/7124          
c   -- var.elim.:  2000/7124          
c   -- var.elim.:  3000/7124          
c   -- var.elim.:  4000/7124          
c   -- var.elim.:  5000/7124          
c   -- var.elim.:  6000/7124          
c   -- var.elim.:  7000/7124          
c   -- var.elim.:  7124/7124          
c   -- var.elim.:  636/636          
c   -- subsuming                       
c   -- var.elim.:  437/437          
c |         0 |   72346   225948 |      --       0       --      -- |     --   | -32429/514
c |         0 |   72346   225948 |   28938       0        0     nan |  0.000 % |
c |       100 |   72287   225430 |   31806      98    12802   130.6 | 53.638 % |
c |       250 |   72287   225430 |   34986     248    35962   145.0 | 53.638 % |
c |       475 |   72287   225430 |   38485     473    79118   167.3 | 53.639 % |
c |       812 |   72249   225023 |   42311     808   147514   182.6 | 53.753 % |
c |      1318 |   72208   224694 |   46516    1310   256407   195.7 | 53.867 % |
c |      2077 |   72208   224694 |   51168    2069   385745   186.4 | 53.867 % |
c ==============================================================================
c (current CPU-time: 86.0119 s)
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2818 |   80914   248412 |   24274    2810   511606   182.1 | 53.867 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15275          
c   -- var.elim.:  2000/15275          
c   -- var.elim.:  3000/15275          
c   -- var.elim.:  4000/15275          
c   -- var.elim.:  5000/15275          
c   -- var.elim.:  6000/15275          
c   -- var.elim.:  7000/15275          
c   -- var.elim.:  8000/15275          
c   -- var.elim.:  9000/15275          
c   -- var.elim.:  10000/15275          
c   -- var.elim.:  11000/15275          
c   -- var.elim.:  12000/15275          
c   -- var.elim.:  13000/15275          
c   -- var.elim.:  14000/15275          
c   -- var.elim.:  15000/15275          
c   -- var.elim.:  15275/15275          
c   -- var.elim.:  1000/6307          
c   -- var.elim.:  2000/6307          
c   -- var.elim.:  3000/6307          
c   -- var.elim.:  4000/6307          
c   -- var.elim.:  5000/6307          
c   -- var.elim.:  6000/6307          
c   -- var.elim.:  6307/6307          
c   -- var.elim.:  71/71          
c   -- subsuming                       
c   -- var.elim.:  1000/5383          
c   -- var.elim.:  2000/5383          
c   -- var.elim.:  3000/5383          
c   -- var.elim.:  4000/5383          
c   -- var.elim.:  5000/5383          
c   -- var.elim.:  5383/5383          
c   -- var.elim.:  871/871          
c |      2818 |   72361   235494 |      --    2810       --      -- |     --   | -8546/-12903
c |      2818 |   72361   235494 |   28944    2810   511606   182.1 | 53.867 % |
c |      2918 |   72361   235494 |   31838    2910   523834   180.0 | 63.245 % |
c |      3068 |   72361   235494 |   35022    3060   556960   182.0 | 63.245 % |
c |      3293 |   72361   235494 |   38524    3285   593762   180.7 | 63.245 % |
c |      3630 |   72284   234607 |   42332    3615   667236   184.6 | 63.426 % |
c |      4136 |   72264   234393 |   46552    4114   748971   182.1 | 63.476 % |
c |      4895 |   72156   233365 |   51131    4865   892118   183.4 | 63.722 % |
c |      6034 |   72046   232480 |   56158    5996  1124761   187.6 | 63.948 % |
c |      7742 |   71624   228499 |   61412    7653  1500853   196.1 | 64.987 % |
c |     10304 |   71502   227294 |   67439   10177  2079188   204.3 | 65.293 % |
c |     14149 |   71104   223602 |   73770   13966  3052355   218.6 | 66.282 % |
c |     19915 |   70764   220363 |   80759   19690  4778030   242.7 | 67.135 % |
c |     28564 |   70142   214644 |   88054   28156  7399647   262.8 | 68.681 % |
c ==============================================================================
c (current CPU-time: 258.462 s)
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38271 |   73559   220011 |   22067   37663 10458505   277.7 | 68.681 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9893          
c   -- var.elim.:  2000/9893          
c   -- var.elim.:  3000/9893          
c   -- var.elim.:  4000/9893          
c   -- var.elim.:  5000/9893          
c   -- var.elim.:  6000/9893          
c   -- var.elim.:  7000/9893          
c   -- var.elim.:  8000/9893          
c   -- var.elim.:  9000/9893          
c   -- var.elim.:  9893/9893          
c   -- var.elim.:  1000/2993          
c   -- var.elim.:  2000/2993          
c   -- var.elim.:  2993/2993          
c   -- var.elim.:  445/445          
c |     38271 |   69562   212432 |      --   37663       --      -- |     --   | -3997/-7578
c |     38271 |   69562   212432 |   27824   37647 10455289   277.7 | 68.681 % |
c |     38371 |   69535   212204 |   30595   37746 10484130   277.8 | 71.122 % |
c |     38522 |   69535   212204 |   33654   37897 10531386   277.9 | 71.122 % |
c |     38747 |   69535   212204 |   37020   38122 10584035   277.6 | 71.122 % |
c |     39085 |   69535   212204 |   40722   38460 10692742   278.0 | 71.122 % |
c |     39591 |   69533   212180 |   44793   38931 10827879   278.1 | 71.127 % |
c |     40350 |   69533   212180 |   49272   39690 11027605   277.8 | 71.126 % |
c |     41489 |   69501   211883 |   54175   40820 11375364   278.7 | 71.200 % |
c |     43197 |   69389   210888 |   59496   42501 11869931   279.3 | 71.458 % |
c |     45759 |   69331   210411 |   65391   45047 12572988   279.1 | 71.594 % |
c |     49603 |   69295   210119 |   71893   48885 13768477   281.7 | 71.682 % |
c |     55369 |   69145   208693 |   78911   54549 15576515   285.6 | 72.038 % |
c |     64018 |   69001   206326 |   86621   63161 18322247   290.1 | 72.374 % |
c |     76992 |   68590   202495 |   94716   75999 22725932   299.0 | 73.343 % |
c |     96453 |   68331   200302 |  103794   95319 29901022   313.7 | 73.967 % |
c ==============================================================================
c (current CPU-time: 781.786 s)
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    109953 |   69212   201973 |   20763  108734 34950410   321.4 | 73.967 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6228          
c   -- var.elim.:  2000/6228          
c   -- var.elim.:  3000/6228          
c   -- var.elim.:  4000/6228          
c   -- var.elim.:  5000/6228          
c   -- var.elim.:  6000/6228          
c   -- var.elim.:  6228/6228          
c   -- var.elim.:  1000/1263          
c   -- var.elim.:  1263/1263          
c |    109953 |   68151   194441 |      --  108734       --      -- |     --   | -1039/-2112
c |    109953 |   68151   194441 |   27260   91446 20619439   225.5 | 73.967 % |
c |    110053 |   68151   194441 |   29986   22786  3812960   167.3 | 74.496 % |
c |    110203 |   68151   194441 |   32985   22936  3846296   167.7 | 74.496 % |
c |    110428 |   68151   194441 |   36283   23161  3910427   168.8 | 74.496 % |
c |    110766 |   68151   194441 |   39911   23499  4004501   170.4 | 74.496 % |
c |    111272 |   68151   194441 |   43903   24005  4168925   173.7 | 74.496 % |
c |    112031 |   68151   194441 |   48293   24764  4377301   176.8 | 74.496 % |
c |    113170 |   68076   193851 |   53064   25900  4668540   180.3 | 74.671 % |
c |    114878 |   68076   193851 |   58370   27608  5097967   184.7 | 74.671 % |
c |    117440 |   68044   193600 |   64177   30163  5909907   195.9 | 74.744 % |
c |    121285 |   67983   193154 |   70532   34003  6968833   204.9 | 74.890 % |
c |    127053 |   67916   192612 |   77508   39755  8397985   211.2 | 75.041 % |
c |    135702 |   67852   192059 |   85179   48396 11225062   231.9 | 75.188 % |
c |    148677 |   67701   190804 |   93488   61321 15369389   250.6 | 75.543 % |
c |    168139 |   67523   189437 |  102567   80684 22273998   276.1 | 75.958 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 C657 -C656 -C655 -C654 -C653 -C652 -C651 C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 C85 -C84 -C83 C82 -C81 -C80 -C79 -C78 -C77 -C76 -C75 -C74 -C73 -C72 -C71 -C70 -C69 -C68 -C67 -C66 -C65 -C64 -C63 -C62 -C61 -C60 -C59 -C58 -C57 -C56 -C55 -C54 -C53 -C52 C51 -C50 -C49 -C48 -C47 -C46 -C45 -C44 -C43 -C42 -C41 -C40 -C39 -C38 -C37 -C36 -C35 -C34 -C33 -C32 -C31 -C30 -C29 -C28 -C27 -C26 -C25 -C24 -C23 C22 -C21 -C20 -C19 -C18 -C17 -C16 -C15 -C14 -C13 -C12 -C11 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 16683
Raw data (stat): 16683 (runsolver) R 16682 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480446151 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 6471 0 0 0 974 24 0 0 25 0 1 0 480446151 26734592 6054 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6527 6054 603 41 0 6486 0
vsize: 26108
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 6487 0 0 0 1974 24 0 0 25 0 1 0 480446151 26902528 6070 4294967295 134512640 134672761 3221224560 3221222608 134566695 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6568 6070 603 41 0 6527 0
vsize: 26272
[startup+30.0027 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 6490 0 0 0 2974 24 0 0 25 0 1 0 480446151 26902528 6073 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6568 6073 603 41 0 6527 0
vsize: 26272
[startup+40.0028 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 6516 0 0 0 3973 25 0 0 25 0 1 0 480446151 26902528 6099 4294967295 134512640 134672761 3221224560 3221222416 134566695 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6568 6099 603 41 0 6527 0
vsize: 26272
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 6526 0 0 0 4972 25 0 0 25 0 1 0 480446151 26902528 6109 4294967295 134512640 134672761 3221224560 3221222992 134605852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6568 6109 603 41 0 6527 0
vsize: 26272
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 6528 0 0 0 5971 25 0 0 25 0 1 0 480446151 26902528 6111 4294967295 134512640 134672761 3221224560 3221223008 134643961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6568 6111 603 41 0 6527 0
vsize: 26272
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 6734 0 0 0 6970 26 0 0 25 0 1 0 480446151 27893760 6317 4294967295 134512640 134672761 3221224560 3221223024 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6810 6317 603 41 0 6769 0
vsize: 27240
[startup+80.0034 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 6734 0 0 0 7971 26 0 0 25 0 1 0 480446151 26902528 6111 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6568 6111 603 41 0 6527 0
vsize: 26272
[startup+90.0038 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 8621 0 0 0 8957 39 0 0 25 0 1 0 480446151 32079872 7067 4294967295 134512640 134672761 3221224560 3221222976 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7832 7067 603 41 0 7791 0
vsize: 31328
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 8621 0 0 0 9899 59 0 0 25 0 1 0 480446151 32079872 7067 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7832 7067 603 41 0 7791 0
vsize: 31328
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 8827 0 0 0 10898 59 0 0 25 0 1 0 480446151 33636352 7273 4294967295 134512640 134672761 3221224560 3221222960 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8212 7273 603 41 0 8171 0
vsize: 32848
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 8828 0 0 0 11898 59 0 0 25 0 1 0 480446151 32079872 7068 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7832 7068 603 41 0 7791 0
vsize: 31328
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16683
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 9524 0 0 0 12894 62 0 0 25 0 1 0 480446151 35069952 7764 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8562 7764 603 41 0 8521 0
vsize: 34248
[startup+140.006 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 16736
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 10268 0 0 0 13892 64 0 0 25 0 1 0 480446151 38236160 8508 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9335 8508 603 41 0 9294 0
vsize: 37340
[startup+150.009 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 16736
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 11024 0 0 0 14890 66 0 0 25 0 1 0 480446151 41234432 9264 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10067 9264 603 41 0 10026 0
vsize: 40268
[startup+160.009 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 16736
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 12086 0 0 0 15888 69 0 0 25 0 1 0 480446151 45670400 10326 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11150 10326 603 41 0 11109 0
vsize: 44600
[startup+170.01 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 16736
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 12913 0 0 0 16887 70 0 0 25 0 1 0 480446151 49029120 11153 4294967295 134512640 134672761 3221224560 3221223600 134612663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11970 11153 603 41 0 11929 0
vsize: 47880
[startup+180.011 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 16736
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 13511 0 0 0 17886 72 0 0 25 0 1 0 480446151 51494912 11751 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12572 11751 603 41 0 12531 0
vsize: 50288
[startup+190.01 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 16736
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 14261 0 0 0 18884 73 0 0 25 0 1 0 480446151 54575104 12501 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13324 12501 603 41 0 13283 0
vsize: 53296
[startup+200.01 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 16736
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 14997 0 0 0 19883 75 0 0 25 0 1 0 480446151 57577472 13237 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14057 13237 603 41 0 14016 0
vsize: 56228
[startup+210.011 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 15667 0 0 0 20881 77 0 0 25 0 1 0 480446151 60338176 13907 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14731 13907 603 41 0 14690 0
vsize: 58924
[startup+220.011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 16189 0 0 0 21880 78 0 0 25 0 1 0 480446151 62427136 14429 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15241 14429 603 41 0 15200 0
vsize: 60964
[startup+230.012 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 17042 0 0 0 22879 80 0 0 25 0 1 0 480446151 65929216 15282 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16096 15282 603 41 0 16055 0
vsize: 64384
[startup+240.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 17685 0 0 0 23877 82 0 0 25 0 1 0 480446151 68681728 15925 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16768 15925 603 41 0 16727 0
vsize: 67072
[startup+250.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 18136 0 0 0 24876 82 0 0 25 0 1 0 480446151 70520832 16376 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17217 16376 603 41 0 17176 0
vsize: 68868
[startup+260.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 20048 0 0 0 25870 88 0 0 25 0 1 0 480446151 80130048 18273 4294967295 134512640 134672761 3221224560 3221222824 1075730078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19563 18273 603 41 0 19522 0
vsize: 78252
[startup+270.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 20609 0 0 0 26841 104 0 0 25 0 1 0 480446151 73428992 17156 4294967295 134512640 134672761 3221224560 3221223008 134643969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17927 17156 603 41 0 17886 0
vsize: 71708
[startup+280.011 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 20950 0 0 0 27840 105 0 0 25 0 1 0 480446151 74792960 17496 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18260 17496 603 41 0 18219 0
vsize: 73040
[startup+290.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 21620 0 0 0 28839 107 0 0 25 0 1 0 480446151 77570048 18166 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18938 18166 603 41 0 18897 0
vsize: 75752
[startup+300.011 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 22134 0 0 0 29837 109 0 0 25 0 1 0 480446151 79683584 18680 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19454 18680 603 41 0 19413 0
vsize: 77816
[startup+310.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 22710 0 0 0 30836 110 0 0 25 0 1 0 480446151 82026496 19256 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20026 19256 603 41 0 19985 0
vsize: 80104
[startup+320.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 23573 0 0 0 31835 111 0 0 25 0 1 0 480446151 85557248 20119 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20888 20119 603 41 0 20847 0
vsize: 83552
[startup+330.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 24137 0 0 0 32835 112 0 0 25 0 1 0 480446151 87773184 20683 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21429 20683 603 41 0 21388 0
vsize: 85716
[startup+340.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 24642 0 0 0 33834 113 0 0 25 0 1 0 480446151 89874432 21188 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21942 21188 603 41 0 21901 0
vsize: 87768
[startup+350.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 25086 0 0 0 34834 113 0 0 25 0 1 0 480446151 91709440 21632 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22390 21632 603 41 0 22349 0
vsize: 89560
[startup+360.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 25621 0 0 0 35833 114 0 0 25 0 1 0 480446151 93818880 22167 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22905 22167 603 41 0 22864 0
vsize: 91620
[startup+370.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 26180 0 0 0 36832 116 0 0 25 0 1 0 480446151 96174080 22726 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23480 22726 603 41 0 23439 0
vsize: 93920
[startup+380.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 26691 0 0 0 37831 117 0 0 25 0 1 0 480446151 98213888 23237 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23978 23237 603 41 0 23937 0
vsize: 95912
[startup+390.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 27293 0 0 0 38829 118 0 0 25 0 1 0 480446151 100659200 23839 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24575 23839 603 41 0 24534 0
vsize: 98300
[startup+400.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 27924 0 0 0 39829 119 0 0 25 0 1 0 480446151 103292928 24470 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25218 24470 603 41 0 25177 0
vsize: 100872
[startup+410.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 28425 0 0 0 40827 121 0 0 25 0 1 0 480446151 105259008 24971 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25698 24971 603 41 0 25657 0
vsize: 102792
[startup+420.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 29103 0 0 0 41825 123 0 0 25 0 1 0 480446151 108126208 25649 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26398 25649 603 41 0 26357 0
vsize: 105592
[startup+430.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 29529 0 0 0 42823 124 0 0 25 0 1 0 480446151 109842432 26075 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26817 26075 603 41 0 26776 0
vsize: 107268
[startup+440.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 29913 0 0 0 43823 125 0 0 25 0 1 0 480446151 111673344 26459 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27264 26459 603 41 0 27223 0
vsize: 109056
[startup+450.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 30450 0 0 0 44822 126 0 0 25 0 1 0 480446151 113868800 26996 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27800 26996 603 41 0 27759 0
vsize: 111200
[startup+460.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 31043 0 0 0 45821 127 0 0 25 0 1 0 480446151 116219904 27589 4294967295 134512640 134672761 3221224560 3221223704 134616126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28374 27589 603 41 0 28333 0
vsize: 113496
[startup+470.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 31478 0 0 0 46819 128 0 0 25 0 1 0 480446151 118030336 28024 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28816 28024 603 41 0 28775 0
vsize: 115264
[startup+480.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16738
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 32081 0 0 0 47818 130 0 0 25 0 1 0 480446151 120516608 28627 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29423 28627 603 41 0 29382 0
vsize: 117692
[startup+490.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 32495 0 0 0 48817 131 0 0 25 0 1 0 480446151 122228736 29041 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29841 29041 603 41 0 29800 0
vsize: 119364
[startup+500.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 32721 0 0 0 49816 132 0 0 25 0 1 0 480446151 123133952 29267 4294967295 134512640 134672761 3221224560 3221223600 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30062 29267 603 41 0 30021 0
vsize: 120248
[startup+510.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 33061 0 0 0 50816 133 0 0 25 0 1 0 480446151 124563456 29607 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30411 29607 603 41 0 30370 0
vsize: 121644
[startup+520.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 33677 0 0 0 51815 134 0 0 25 0 1 0 480446151 127041536 30223 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31016 30223 603 41 0 30975 0
vsize: 124064
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 34071 0 0 0 52813 136 0 0 25 0 1 0 480446151 128630784 30617 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31404 30617 603 41 0 31363 0
vsize: 125616
[startup+540.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 34534 0 0 0 53813 137 0 0 25 0 1 0 480446151 130592768 31080 4294967295 134512640 134672761 3221224560 3221223704 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31883 31080 603 41 0 31842 0
vsize: 127532
[startup+550.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 34887 0 0 0 54812 137 0 0 25 0 1 0 480446151 131932160 31433 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31433 603 41 0 32169 0
vsize: 128840
[startup+560.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 35292 0 0 0 55811 138 0 0 25 0 1 0 480446151 133668864 31838 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32634 31838 603 41 0 32593 0
vsize: 130536
[startup+570.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 36067 0 0 0 56810 140 0 0 25 0 1 0 480446151 136769536 32613 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33391 32613 603 41 0 33350 0
vsize: 133564
[startup+580.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 36666 0 0 0 57809 141 0 0 25 0 1 0 480446151 139251712 33212 4294967295 134512640 134672761 3221224560 3221223696 134614736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33997 33212 603 41 0 33956 0
vsize: 135988
[startup+590.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 37134 0 0 0 58808 142 0 0 25 0 1 0 480446151 141176832 33680 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34467 33680 603 41 0 34426 0
vsize: 137868
[startup+600.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 37819 0 0 0 59806 144 0 0 25 0 1 0 480446151 144007168 34365 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35158 34365 603 41 0 35117 0
vsize: 140632
[startup+610.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 38466 0 0 0 60804 146 0 0 25 0 1 0 480446151 146636800 35012 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35800 35012 603 41 0 35759 0
vsize: 143200
[startup+620.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 38849 0 0 0 61803 148 0 0 25 0 1 0 480446151 148209664 35395 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36184 35395 603 41 0 36143 0
vsize: 144736
[startup+630.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 39428 0 0 0 62802 149 0 0 25 0 1 0 480446151 150532096 35974 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36751 35974 603 41 0 36710 0
vsize: 147004
[startup+640.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 39988 0 0 0 63800 151 0 0 25 0 1 0 480446151 152838144 36534 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37314 36534 603 41 0 37273 0
vsize: 149256
[startup+650.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 40427 0 0 0 64800 152 0 0 25 0 1 0 480446151 154570752 36973 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37737 36973 603 41 0 37696 0
vsize: 150948
[startup+660.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 40740 0 0 0 65799 152 0 0 25 0 1 0 480446151 155873280 37286 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38055 37286 603 41 0 38014 0
vsize: 152220
[startup+670.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 41247 0 0 0 66798 154 0 0 25 0 1 0 480446151 157970432 37793 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38567 37793 603 41 0 38526 0
vsize: 154268
[startup+680.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 41634 0 0 0 67798 154 0 0 25 0 1 0 480446151 159502336 38180 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38941 38180 603 41 0 38900 0
vsize: 155764
[startup+690.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 42161 0 0 0 68797 155 0 0 25 0 1 0 480446151 161697792 38707 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39477 38707 603 41 0 39436 0
vsize: 157908
[startup+700.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 42440 0 0 0 69796 156 0 0 25 0 1 0 480446151 162889728 38986 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39768 38986 603 41 0 39727 0
vsize: 159072
[startup+710.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 42682 0 0 0 70795 157 0 0 25 0 1 0 480446151 163819520 39228 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39995 39228 603 41 0 39954 0
vsize: 159980
[startup+720.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 43178 0 0 0 71794 158 0 0 25 0 1 0 480446151 165904384 39724 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40504 39724 603 41 0 40463 0
vsize: 162016
[startup+730.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 43739 0 0 0 72793 159 0 0 25 0 1 0 480446151 168099840 40285 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41040 40285 603 41 0 40999 0
vsize: 164160
[startup+740.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 44286 0 0 0 73793 159 0 0 25 0 1 0 480446151 170446848 40832 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41613 40832 603 41 0 41572 0
vsize: 166452
[startup+750.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 44935 0 0 0 74791 161 0 0 25 0 1 0 480446151 173023232 41481 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42242 41481 603 41 0 42201 0
vsize: 168968
[startup+760.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 45426 0 0 0 75789 163 0 0 25 0 1 0 480446151 175095808 41972 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42748 41972 603 41 0 42707 0
vsize: 170992
[startup+770.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 45687 0 0 0 76789 164 0 0 25 0 1 0 480446151 176123904 42233 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42999 42233 603 41 0 42958 0
vsize: 171996
[startup+780.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 45939 0 0 0 77789 164 0 0 25 0 1 0 480446151 177172480 42485 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43255 42485 603 41 0 43214 0
vsize: 173020
[startup+790.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48158 0 0 0 78772 180 0 0 25 0 1 0 480446151 178049024 42733 4294967295 134512640 134672761 3221224560 3221223816 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43469 42733 603 41 0 43428 0
vsize: 173876
[startup+800.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48397 0 0 0 79772 181 0 0 25 0 1 0 480446151 178573312 42818 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42818 603 41 0 43556 0
vsize: 174388
[startup+810.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48397 0 0 0 80772 181 0 0 25 0 1 0 480446151 178573312 42818 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42818 603 41 0 43556 0
vsize: 174388
[startup+820.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48397 0 0 0 81772 181 0 0 25 0 1 0 480446151 178573312 42818 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42818 603 41 0 43556 0
vsize: 174388
[startup+830.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48397 0 0 0 82773 181 0 0 25 0 1 0 480446151 178573312 42818 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42818 603 41 0 43556 0
vsize: 174388
[startup+840.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48397 0 0 0 83773 181 0 0 25 0 1 0 480446151 178573312 42818 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42818 603 41 0 43556 0
vsize: 174388
[startup+850.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48397 0 0 0 84773 181 0 0 25 0 1 0 480446151 178573312 42818 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42818 603 41 0 43556 0
vsize: 174388
[startup+860.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48397 0 0 0 85773 181 0 0 25 0 1 0 480446151 178573312 42818 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42818 603 41 0 43556 0
vsize: 174388
[startup+870.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 86773 181 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+880.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 87774 181 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+890.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 88774 181 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+900.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 89774 181 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+910.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 90774 181 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+920.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 91774 181 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+930.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 92774 181 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223760 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+940.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 93774 181 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+950.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 94774 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+960.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 95775 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+970.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 96775 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+980.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 97775 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+990.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 98775 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 99776 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 100776 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223432 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 101776 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223704 134616320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 102776 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 103776 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 104776 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 105777 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 106777 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 107777 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223712 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 108777 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 109777 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 110777 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 111778 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 112778 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 113778 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223704 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 114778 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 115778 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 116778 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 117778 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1190.03 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 118779 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1200.03 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 119779 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
[startup+1210.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 16740
Raw data (stat): 16683 (minisat+) R 16682 11931 11930 0 -1 0 48398 0 0 0 120779 182 0 0 25 0 1 0 480446151 178573312 42819 4294967295 134512640 134672761 3221224560 3221223600 134613740 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43597 42819 603 41 0 43556 0
vsize: 174388
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.14 s]
Raw data (loadavg): 1.05 1.01 0.93 1/54 16740
Raw data (stat): 16683 (minisat+) Z 16682 11931 11930 0 -1 12 48399 0 0 0 120779 193 0 0 25 0 1 0 480446151 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.14
CPU time (s): 1209.73
CPU user time (s): 1207.8
CPU system time (s): 1.9347
CPU usage (%): 99.9658
Max. virtual memory (Kb): 174388
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####