PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 01:01:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4092 boxname=wulflinc17 idbench=332 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2b591d1b24a201f365bc505135aa0578  /oldhome/oroussel/tmp/wulflinc17/normalized-frb45-21-4.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-frb45-21-4.opb /oldhome/oroussel/tmp/wulflinc17/normalized-frb45-21-4.opb
IDLAUNCH: 4092
/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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        823412 kB
Buffers:         35728 kB
Cached:         140396 kB
SwapCached:       2376 kB
Active:          59584 kB
Inactive:       121868 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        823132 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            24048 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:21:18 (client local time) WITH STATUS 10 IN 1200.31 SECONDS
stats: 4092 7 1200.31 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58549 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   58549   117098 |   17564       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   58549   117098 |   23419       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 2.75558 s)
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  104166   224223 |   31249       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/31196          
c   -- var.elim.:  2000/31196          
c   -- var.elim.:  3000/31196          
c   -- var.elim.:  4000/31196          
c   -- var.elim.:  5000/31196          
c   -- var.elim.:  6000/31196          
c   -- var.elim.:  7000/31196          
c   -- var.elim.:  8000/31196          
c   -- var.elim.:  9000/31196          
c   -- var.elim.:  10000/31196          
c   -- var.elim.:  11000/31196          
c   -- var.elim.:  12000/31196          
c   -- var.elim.:  13000/31196          
c   -- var.elim.:  14000/31196          
c   -- var.elim.:  15000/31196          
c   -- var.elim.:  16000/31196          
c   -- var.elim.:  17000/31196          
c   -- var.elim.:  18000/31196          
c   -- var.elim.:  19000/31196          
c   -- var.elim.:  20000/31196          
c   -- var.elim.:  21000/31196          
c   -- var.elim.:  22000/31196          
c   -- var.elim.:  23000/31196          
c   -- var.elim.:  24000/31196          
c   -- var.elim.:  25000/31196          
c   -- var.elim.:  26000/31196          
c   -- var.elim.:  27000/31196          
c   -- var.elim.:  28000/31196          
c   -- var.elim.:  29000/31196          
c   -- var.elim.:  30000/31196          
c   -- var.elim.:  31000/31196          
c   -- var.elim.:  31196/31196          
c   -- var.elim.:  1000/15829          
c   -- var.elim.:  2000/15829          
c   -- var.elim.:  3000/15829          
c   -- var.elim.:  4000/15829          
c   -- var.elim.:  5000/15829          
c   -- var.elim.:  6000/15829          
c   -- var.elim.:  7000/15829          
c   -- var.elim.:  8000/15829          
c   -- var.elim.:  9000/15829          
c   -- var.elim.:  10000/15829          
c   -- var.elim.:  11000/15829          
c   -- var.elim.:  12000/15829          
c   -- var.elim.:  13000/15829          
c   -- var.elim.:  14000/15829          
c   -- var.elim.:  15000/15829          
c   -- var.elim.:  15829/15829          
c   -- var.elim.:  1000/2532          
c   -- var.elim.:  2000/2532          
c   -- var.elim.:  2532/2532          
c   -- subsuming                       
c   -- var.elim.:  1000/6085          
c   -- var.elim.:  2000/6085          
c   -- var.elim.:  3000/6085          
c   -- var.elim.:  4000/6085          
c   -- var.elim.:  5000/6085          
c   -- var.elim.:  6000/6085          
c   -- var.elim.:  6085/6085          
c   -- var.elim.:  640/640          
c   -- subsuming                       
c   -- var.elim.:  471/471          
c |         0 |   71884   224353 |      --       0       --      -- |     --   | -32282/131
c |         0 |   71884   224353 |   28753       0        0     nan |  0.000 % |
c |       100 |   71858   224147 |   31617      99    16250   164.1 | 53.177 % |
c |       250 |   71826   223852 |   34763     245    29714   121.3 | 53.279 % |
c |       475 |   71826   223852 |   38240     470    61776   131.4 | 53.279 % |
c |       812 |   71826   223852 |   42064     807   107523   133.2 | 53.279 % |
c |      1320 |   71826   223852 |   46270    1315   196920   149.7 | 53.279 % |
c |      2079 |   71826   223852 |   50897    2074   365346   176.2 | 53.279 % |
c |      3218 |   71826   223852 |   55987    3213   546414   170.1 | 53.279 % |
c |      4926 |   71591   221565 |   61384    4899   858696   175.3 | 53.995 % |
c |      7488 |   71234   218146 |   67186    7428  1383574   186.3 | 55.010 % |
c |     11332 |   70934   215585 |   73593   11225  2339198   208.4 | 55.924 % |
c |     17099 |   70628   212944 |   80603   16913  3912567   231.3 | 56.888 % |
c ==============================================================================
c (current CPU-time: 151.434 s)
c ==============================================================================
c [1mFound solution: -34[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 |     24957 |   71175   211078 |   21352   24617  6281292   255.2 | 56.888 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7439          
c   -- var.elim.:  2000/7439          
c   -- var.elim.:  3000/7439          
c   -- var.elim.:  4000/7439          
c   -- var.elim.:  5000/7439          
c   -- var.elim.:  6000/7439          
c   -- var.elim.:  7000/7439          
c   -- var.elim.:  7439/7439          
c   -- var.elim.:  1000/1665          
c   -- var.elim.:  1665/1665          
c |     24957 |   69982   208066 |      --   24617       --      -- |     --   | -1185/-1677
c |     24957 |   69982   208066 |   27992   22438  4496996   200.4 | 56.888 % |
c |     25058 |   69982   208066 |   30792   22539  4520663   200.6 | 59.977 % |
c |     25208 |   69954   207830 |   33857   22688  4556674   200.8 | 60.063 % |
c |     25433 |   69920   207511 |   37225   22904  4638011   202.5 | 60.169 % |
c ==============================================================================
c (current CPU-time: 160.981 s)
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     25568 |   75935   223619 |   22780   23039  4669116   202.7 | 60.169 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10490          
c   -- var.elim.:  2000/10490          
c   -- var.elim.:  3000/10490          
c   -- var.elim.:  4000/10490          
c   -- var.elim.:  5000/10490          
c   -- var.elim.:  6000/10490          
c   -- var.elim.:  7000/10490          
c   -- var.elim.:  8000/10490          
c   -- var.elim.:  9000/10490          
c   -- var.elim.:  10000/10490          
c   -- var.elim.:  10490/10490          
c   -- var.elim.:  1000/4071          
c   -- var.elim.:  2000/4071          
c   -- var.elim.:  3000/4071          
c   -- var.elim.:  4000/4071          
c   -- var.elim.:  4071/4071          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c   -- var.elim.:  1000/4035          
c   -- var.elim.:  2000/4035          
c   -- var.elim.:  3000/4035          
c   -- var.elim.:  4000/4035          
c   -- var.elim.:  4035/4035          
c   -- var.elim.:  746/746          
c |     25568 |   70041   214387 |      --   23039       --      -- |     --   | -5878/-9057
c |     25568 |   70041   214387 |   28016   22810  4412571   193.4 | 60.169 % |
c |     25668 |   70041   214387 |   30818   22910  4434698   193.6 | 67.138 % |
c |     25818 |   70039   214364 |   33898   23059  4472255   193.9 | 67.142 % |
c |     26043 |   70039   214364 |   37288   23284  4521842   194.2 | 67.142 % |
c |     26380 |   70039   214364 |   41017   23621  4612728   195.3 | 67.143 % |
c |     26886 |   70039   214364 |   45119   24127  4783251   198.3 | 67.142 % |
c |     27645 |   69999   213988 |   49602   24874  5027283   202.1 | 67.244 % |
c |     28785 |   69971   213744 |   54541   25994  5304263   204.1 | 67.315 % |
c |     30496 |   69853   212572 |   59894   27695  5934048   214.3 | 67.615 % |
c |     33059 |   69853   212572 |   65883   30258  6759566   223.4 | 67.615 % |
c |     36903 |   69853   212572 |   72472   34102  7981314   234.0 | 67.615 % |
c |     42669 |   69629   210484 |   79463   39792  9830651   247.1 | 68.184 % |
c |     51318 |   69178   206373 |   86844   48280 12768171   264.5 | 69.296 % |
c |     64292 |   69037   205078 |   95333   61113 17868190   292.4 | 69.652 % |
c |     83753 |   68632   201493 |  104251   80360 25661226   319.3 | 70.663 % |
c ==============================================================================
c (current CPU-time: 532.139 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 |     87489 |   70148   205317 |   21044   84082 27061151   321.8 | 70.663 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6359          
c   -- var.elim.:  2000/6359          
c   -- var.elim.:  3000/6359          
c   -- var.elim.:  4000/6359          
c   -- var.elim.:  5000/6359          
c   -- var.elim.:  6000/6359          
c   -- var.elim.:  6359/6359          
c   -- var.elim.:  1000/1024          
c   -- var.elim.:  1024/1024          
c   -- var.elim.:  428/428          
c |     87489 |   68642   203299 |      --   84082       --      -- |     --   | -1506/-2017
c |     87489 |   68642   203299 |   27456   83612 26746218   319.9 | 70.663 % |
c |     87589 |   68642   203299 |   30202   23499  5099533   217.0 | 70.872 % |
c |     87739 |   68614   203039 |   33209   23646  5129212   216.9 | 70.943 % |
c |     87965 |   68612   203018 |   36529   23871  5200348   217.9 | 70.948 % |
c |     88302 |   68612   203018 |   40181   24208  5338812   220.5 | 70.948 % |
c |     88808 |   68580   202719 |   44179   24708  5513331   223.1 | 71.024 % |
c |     89567 |   68580   202719 |   48597   25467  5727899   224.9 | 71.024 % |
c |     90706 |   68578   202695 |   53455   26603  6135732   230.6 | 71.029 % |
c |     92414 |   68540   202398 |   58768   28307  6721827   237.5 | 71.125 % |
c |     94976 |   68538   202374 |   64643   30865  7561064   245.0 | 71.130 % |
c ==============================================================================
c (current CPU-time: 579.844 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 |     96581 |   68538   202068 |   20561   32466  8090930   249.2 | 71.130 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4193          
c   -- var.elim.:  2000/4193          
c   -- var.elim.:  3000/4193          
c   -- var.elim.:  4000/4193          
c   -- var.elim.:  4193/4193          
c   -- var.elim.:  87/87          
c |     96581 |   68475   197487 |      --   32466       --      -- |     --   | -43/-44
c |     96581 |   68475   197487 |   27390   29842  5529573   185.3 | 71.130 % |
c |     96683 |   68475   197487 |   30129   29944  5574852   186.2 | 71.284 % |
c |     96833 |   68475   197487 |   33141   30094  5622763   186.8 | 71.284 % |
c |     97058 |   68475   197487 |   36456   30319  5669103   187.0 | 71.284 % |
c |     97395 |   68475   197487 |   40101   30656  5756016   187.8 | 71.284 % |
c |     97901 |   68475   197487 |   44111   31162  5883704   188.8 | 71.284 % |
c |     98661 |   68475   197487 |   48523   31922  6111681   191.5 | 71.284 % |
c |     99800 |   68447   197271 |   53353   33057  6467277   195.6 | 71.354 % |
c |    101508 |   68445   197249 |   58687   34762  7257302   208.8 | 71.359 % |
c |    104070 |   68417   197025 |   64529   37319  8063706   216.1 | 71.430 % |
c |    107914 |   68286   195931 |   70846   41127  9340458   227.1 | 71.743 % |
c |    113680 |   68178   195039 |   77807   46859 11245231   240.0 | 72.016 % |
c |    122329 |   68066   194124 |   85448   55468 14046757   253.2 | 72.294 % |
c |    135303 |   67920   192804 |   93791   68407 18696150   273.3 | 72.637 % |
c |    154764 |   67617   190166 |  102710   87816 26026875   296.4 | 73.370 % |
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 -#### 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): 1.00 1.01 0.93 2/55 27351
Raw data (stat): 27351 (runsolver) R 27350 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480476552 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.0007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 6481 0 0 0 973 25 0 0 25 0 1 0 480476552 26783744 6069 4294967295 134512640 134672761 3221224560 3221222992 134604069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6539 6069 603 41 0 6498 0
vsize: 26156
[startup+20.0011 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 6493 0 0 0 1973 25 0 0 25 0 1 0 480476552 26959872 6081 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6582 6081 603 41 0 6541 0
vsize: 26328
[startup+30.0013 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 6498 0 0 0 2973 25 0 0 25 0 1 0 480476552 26959872 6086 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6582 6086 603 41 0 6541 0
vsize: 26328
[startup+40.0013 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 6505 0 0 0 3973 25 0 0 25 0 1 0 480476552 26959872 6093 4294967295 134512640 134672761 3221224560 3221222816 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6582 6093 603 41 0 6541 0
vsize: 26328
[startup+50.0018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 6522 0 0 0 4973 25 0 0 25 0 1 0 480476552 26959872 6110 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6582 6110 603 41 0 6541 0
vsize: 26328
[startup+60.0012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 6528 0 0 0 5973 25 0 0 25 0 1 0 480476552 26959872 6116 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6582 6116 603 41 0 6541 0
vsize: 26328
[startup+70.001 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 6732 0 0 0 6972 26 0 0 25 0 1 0 480476552 27910144 6320 4294967295 134512640 134672761 3221224560 3221223056 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6814 6320 603 41 0 6773 0
vsize: 27256
[startup+80.0017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 6732 0 0 0 7972 26 0 0 25 0 1 0 480476552 26959872 6116 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6582 6116 603 41 0 6541 0
vsize: 26328
[startup+90.001 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 7438 0 0 0 8971 28 0 0 25 0 1 0 480476552 29057024 6618 4294967295 134512640 134672761 3221224560 3221223504 134606475 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7094 6618 603 41 0 7053 0
vsize: 28376
[startup+100.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 8307 0 0 0 9969 30 0 0 25 0 1 0 480476552 32751616 7487 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7996 7487 603 41 0 7955 0
vsize: 31984
[startup+110.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 9350 0 0 0 10967 32 0 0 25 0 1 0 480476552 36954112 8530 4294967295 134512640 134672761 3221224560 3221223744 134610778 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9022 8530 603 41 0 8981 0
vsize: 36088
[startup+120.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 10276 0 0 0 11965 35 0 0 25 0 1 0 480476552 40701952 9456 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9937 9456 603 41 0 9896 0
vsize: 39748
[startup+130.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 11111 0 0 0 12963 36 0 0 25 0 1 0 480476552 44257280 10291 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10805 10291 603 41 0 10764 0
vsize: 43220
[startup+140.001 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 11790 0 0 0 13963 37 0 0 25 0 1 0 480476552 47001600 10970 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11475 10970 603 41 0 11434 0
vsize: 45900
[startup+150.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 12787 0 0 0 14960 40 0 0 25 0 1 0 480476552 51118080 11967 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12480 11967 603 41 0 12439 0
vsize: 49920
[startup+160.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 14200 0 0 0 15951 49 0 0 25 0 1 0 480476552 55848960 12657 4294967295 134512640 134672761 3221224560 3221223600 134612659 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13635 12657 603 41 0 13594 0
vsize: 54540
[startup+170.001 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 15556 0 0 0 16929 70 0 0 25 0 1 0 480476552 55971840 12841 4294967295 134512640 134672761 3221224560 3221223008 134644038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13665 12841 603 41 0 13624 0
vsize: 54660
[startup+180.001 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 15760 0 0 0 17928 71 0 0 25 0 1 0 480476552 55971840 12841 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13665 12841 603 41 0 13624 0
vsize: 54660
[startup+190.001 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 15760 0 0 0 18928 71 0 0 25 0 1 0 480476552 55971840 12841 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13665 12841 603 41 0 13624 0
vsize: 54660
[startup+200.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 15763 0 0 0 19928 71 0 0 25 0 1 0 480476552 55971840 12844 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13665 12844 603 41 0 13624 0
vsize: 54660
[startup+210.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 16323 0 0 0 20927 72 0 0 25 0 1 0 480476552 58335232 13404 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14242 13404 603 41 0 14201 0
vsize: 56968
[startup+220.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 17315 0 0 0 21926 74 0 0 25 0 1 0 480476552 62484480 14396 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15255 14396 603 41 0 15214 0
vsize: 61020
[startup+230.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 17920 0 0 0 22925 75 0 0 25 0 1 0 480476552 64987136 15001 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15866 15001 603 41 0 15825 0
vsize: 63464
[startup+240.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 18576 0 0 0 23923 76 0 0 25 0 1 0 480476552 67653632 15657 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16517 15657 603 41 0 16476 0
vsize: 66068
[startup+250.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27353
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 19365 0 0 0 24922 78 0 0 25 0 1 0 480476552 70889472 16446 4294967295 134512640 134672761 3221224560 3221223704 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17307 16446 603 41 0 17266 0
vsize: 69228
[startup+260.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27355
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 19980 0 0 0 25921 79 0 0 25 0 1 0 480476552 73334784 17061 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17904 17061 603 41 0 17863 0
vsize: 71616
[startup+270.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27355
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 20568 0 0 0 26920 80 0 0 25 0 1 0 480476552 75784192 17649 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18502 17649 603 41 0 18461 0
vsize: 74008
[startup+280.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 21132 0 0 0 27919 81 0 0 25 0 1 0 480476552 78024704 18213 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18213 603 41 0 19008 0
vsize: 76196
[startup+290.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 21887 0 0 0 28917 83 0 0 25 0 1 0 480476552 81141760 18968 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19810 18968 603 41 0 19769 0
vsize: 79240
[startup+300.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 22552 0 0 0 29915 86 0 0 25 0 1 0 480476552 83894272 19633 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20482 19633 603 41 0 20441 0
vsize: 81928
[startup+310.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 23520 0 0 0 30913 88 0 0 25 0 1 0 480476552 87871488 20601 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21453 20601 603 41 0 21412 0
vsize: 85812
[startup+320.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 24388 0 0 0 31911 90 0 0 25 0 1 0 480476552 91369472 21469 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22307 21469 603 41 0 22266 0
vsize: 89228
[startup+330.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 25194 0 0 0 32909 92 0 0 25 0 1 0 480476552 94625792 22275 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23102 22275 603 41 0 23061 0
vsize: 92408
[startup+340.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 25947 0 0 0 33908 94 0 0 25 0 1 0 480476552 97767424 23028 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23869 23028 603 41 0 23828 0
vsize: 95476
[startup+350.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 26363 0 0 0 34907 94 0 0 25 0 1 0 480476552 99491840 23444 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24290 23444 603 41 0 24249 0
vsize: 97160
[startup+360.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 27140 0 0 0 35906 96 0 0 25 0 1 0 480476552 102633472 24221 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25057 24221 603 41 0 25016 0
vsize: 100228
[startup+370.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 27698 0 0 0 36905 97 0 0 25 0 1 0 480476552 104955904 24779 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25624 24779 603 41 0 25583 0
vsize: 102496
[startup+380.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 28618 0 0 0 37904 99 0 0 25 0 1 0 480476552 108707840 25699 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26540 25699 603 41 0 26499 0
vsize: 106160
[startup+390.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 29161 0 0 0 38903 100 0 0 25 0 1 0 480476552 110940160 26242 4294967295 134512640 134672761 3221224560 3221223600 134612963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27085 26243 603 41 0 27044 0
vsize: 108340
[startup+400.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 29585 0 0 0 39902 101 0 0 25 0 1 0 480476552 112852992 26666 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27552 26666 603 41 0 27511 0
vsize: 110208
[startup+410.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 30270 0 0 0 40900 103 0 0 25 0 1 0 480476552 115675136 27351 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28241 27351 603 41 0 28200 0
vsize: 112964
[startup+420.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 31046 0 0 0 41899 105 0 0 25 0 1 0 480476552 118878208 28127 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29023 28127 603 41 0 28982 0
vsize: 116092
[startup+430.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 31748 0 0 0 42897 107 0 0 25 0 1 0 480476552 121757696 28829 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29726 28829 603 41 0 29685 0
vsize: 118904
[startup+440.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 32197 0 0 0 43896 108 0 0 25 0 1 0 480476552 123588608 29278 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30173 29278 603 41 0 30132 0
vsize: 120692
[startup+450.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 32700 0 0 0 44895 109 0 0 25 0 1 0 480476552 125640704 29781 4294967295 134512640 134672761 3221224560 3221223568 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30674 29781 603 41 0 30633 0
vsize: 122696
[startup+460.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 33361 0 0 0 45894 110 0 0 25 0 1 0 480476552 128335872 30442 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31332 30442 603 41 0 31291 0
vsize: 125328
[startup+470.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 33711 0 0 0 46893 111 0 0 25 0 1 0 480476552 129798144 30792 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31689 30792 603 41 0 31648 0
vsize: 126756
[startup+480.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 34151 0 0 0 47892 113 0 0 25 0 1 0 480476552 131596288 31232 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32128 31232 603 41 0 32087 0
vsize: 128512
[startup+490.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 34556 0 0 0 48891 113 0 0 25 0 1 0 480476552 133152768 31637 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32508 31637 603 41 0 32467 0
vsize: 130032
[startup+500.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 35165 0 0 0 49890 115 0 0 25 0 1 0 480476552 135671808 32246 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33123 32246 603 41 0 33082 0
vsize: 132492
[startup+510.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 35849 0 0 0 50889 116 0 0 25 0 1 0 480476552 138526720 32930 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33820 32930 603 41 0 33779 0
vsize: 135280
[startup+520.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 36287 0 0 0 51889 117 0 0 25 0 1 0 480476552 140226560 33368 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34235 33368 603 41 0 34194 0
vsize: 136940
[startup+530.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 36862 0 0 0 52889 118 0 0 25 0 1 0 480476552 142606336 33943 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34816 33943 603 41 0 34775 0
vsize: 139264
[startup+540.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 38863 0 0 0 53875 131 0 0 25 0 1 0 480476552 143663104 34233 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35074 34233 603 41 0 35033 0
vsize: 140296
[startup+550.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27357
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 39052 0 0 0 54874 132 0 0 25 0 1 0 480476552 143986688 34308 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35153 34308 603 41 0 35112 0
vsize: 140612
[startup+560.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 39052 0 0 0 55874 132 0 0 25 0 1 0 480476552 143986688 34308 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35153 34308 603 41 0 35112 0
vsize: 140612
[startup+570.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 39052 0 0 0 56875 132 0 0 25 0 1 0 480476552 143986688 34308 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35153 34308 603 41 0 35112 0
vsize: 140612
[startup+580.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 39052 0 0 0 57875 132 0 0 25 0 1 0 480476552 143986688 34308 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35153 34308 603 41 0 35112 0
vsize: 140612
[startup+590.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40287 0 0 0 58866 142 0 0 25 0 1 0 480476552 143814656 34266 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34266 603 41 0 35070 0
vsize: 140444
[startup+600.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40287 0 0 0 59866 142 0 0 25 0 1 0 480476552 143814656 34266 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34266 603 41 0 35070 0
vsize: 140444
[startup+610.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40287 0 0 0 60866 142 0 0 25 0 1 0 480476552 143814656 34266 4294967295 134512640 134672761 3221224560 3221223600 134614301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34266 603 41 0 35070 0
vsize: 140444
[startup+620.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40287 0 0 0 61866 142 0 0 25 0 1 0 480476552 143814656 34266 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34266 603 41 0 35070 0
vsize: 140444
[startup+630.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 62867 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+640.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 63867 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+650.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 64867 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+660.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 65867 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223600 134613769 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+670.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 66867 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+680.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 67867 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+690.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 68868 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223600 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+700.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 69868 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+710.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 70868 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+720.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 71868 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+730.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 72868 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+740.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 73868 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223664 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+750.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 74869 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+760.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 75869 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+770.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 76869 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+780.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 77869 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+790.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 78869 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+800.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 79869 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+810.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 80870 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+820.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 81870 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+830.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 82870 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223716 134564777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+840.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 83870 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+850.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27359
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 84870 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223600 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+860.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 85871 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+870.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 86871 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+880.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40288 0 0 0 87871 142 0 0 25 0 1 0 480476552 143814656 34267 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34267 603 41 0 35070 0
vsize: 140444
[startup+890.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40289 0 0 0 88871 142 0 0 25 0 1 0 480476552 143814656 34268 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34268 603 41 0 35070 0
vsize: 140444
[startup+900.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40289 0 0 0 89871 142 0 0 25 0 1 0 480476552 143814656 34268 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34268 603 41 0 35070 0
vsize: 140444
[startup+910.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40289 0 0 0 90872 142 0 0 25 0 1 0 480476552 143814656 34268 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34268 603 41 0 35070 0
vsize: 140444
[startup+920.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40290 0 0 0 91872 142 0 0 25 0 1 0 480476552 143814656 34269 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34269 603 41 0 35070 0
vsize: 140444
[startup+930.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40291 0 0 0 92872 142 0 0 25 0 1 0 480476552 143814656 34270 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34270 603 41 0 35070 0
vsize: 140444
[startup+940.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40292 0 0 0 93872 142 0 0 25 0 1 0 480476552 143814656 34271 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34271 603 41 0 35070 0
vsize: 140444
[startup+950.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40293 0 0 0 94872 142 0 0 25 0 1 0 480476552 143814656 34272 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35111 34272 603 41 0 35070 0
vsize: 140444
[startup+960.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40537 0 0 0 95872 143 0 0 25 0 1 0 480476552 144855040 34516 4294967295 134512640 134672761 3221224560 3221223504 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35365 34516 603 41 0 35324 0
vsize: 141460
[startup+970.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 40861 0 0 0 96871 144 0 0 25 0 1 0 480476552 146161664 34840 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35684 34840 603 41 0 35643 0
vsize: 142736
[startup+980.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 41126 0 0 0 97871 145 0 0 25 0 1 0 480476552 147324928 35105 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35968 35105 603 41 0 35927 0
vsize: 143872
[startup+990.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 41877 0 0 0 98869 147 0 0 25 0 1 0 480476552 150446080 35856 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36730 35856 603 41 0 36689 0
vsize: 146920
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 42312 0 0 0 99868 148 0 0 25 0 1 0 480476552 152150016 36291 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37146 36291 603 41 0 37105 0
vsize: 148584
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 42731 0 0 0 100867 149 0 0 25 0 1 0 480476552 153833472 36710 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37557 36710 603 41 0 37516 0
vsize: 150228
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 43097 0 0 0 101866 150 0 0 25 0 1 0 480476552 155410432 37076 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37942 37076 603 41 0 37901 0
vsize: 151768
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 43436 0 0 0 102865 151 0 0 25 0 1 0 480476552 156835840 37415 4294967295 134512640 134672761 3221224560 3221223364 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38290 37415 603 41 0 38249 0
vsize: 153160
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 44022 0 0 0 103865 152 0 0 25 0 1 0 480476552 159191040 38001 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38865 38001 603 41 0 38824 0
vsize: 155460
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 44338 0 0 0 104864 153 0 0 25 0 1 0 480476552 160501760 38317 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39185 38317 603 41 0 39144 0
vsize: 156740
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 44811 0 0 0 105863 154 0 0 25 0 1 0 480476552 162443264 38790 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39659 38790 603 41 0 39618 0
vsize: 158636
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 45121 0 0 0 106863 155 0 0 25 0 1 0 480476552 163741696 39100 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39976 39100 603 41 0 39935 0
vsize: 159904
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 45548 0 0 0 107861 156 0 0 25 0 1 0 480476552 165470208 39527 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40398 39527 603 41 0 40357 0
vsize: 161592
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 46039 0 0 0 108860 158 0 0 25 0 1 0 480476552 167387136 40018 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40866 40018 603 41 0 40825 0
vsize: 163464
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 46388 0 0 0 109859 158 0 0 25 0 1 0 480476552 168947712 40367 4294967295 134512640 134672761 3221224560 3221223704 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41247 40367 603 41 0 41206 0
vsize: 164988
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 46677 0 0 0 110859 159 0 0 25 0 1 0 480476552 170139648 40656 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41538 40656 603 41 0 41497 0
vsize: 166152
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 46940 0 0 0 111859 160 0 0 25 0 1 0 480476552 171180032 40919 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41792 40919 603 41 0 41751 0
vsize: 167168
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 47435 0 0 0 112858 161 0 0 25 0 1 0 480476552 173223936 41414 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42291 41414 603 41 0 42250 0
vsize: 169164
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 47778 0 0 0 113857 162 0 0 25 0 1 0 480476552 174534656 41757 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42611 41757 603 41 0 42570 0
vsize: 170444
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27361
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 48065 0 0 0 114857 162 0 0 25 0 1 0 480476552 175718400 42044 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42900 42044 603 41 0 42859 0
vsize: 171600
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27363
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 48441 0 0 0 115857 163 0 0 25 0 1 0 480476552 177307648 42420 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43288 42420 603 41 0 43247 0
vsize: 173152
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27363
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 49034 0 0 0 116856 164 0 0 25 0 1 0 480476552 179752960 43013 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43885 43013 603 41 0 43844 0
vsize: 175540
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27363
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 49533 0 0 0 117855 165 0 0 25 0 1 0 480476552 181846016 43512 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44396 43512 603 41 0 44355 0
vsize: 177584
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27363
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 50097 0 0 0 118853 167 0 0 25 0 1 0 480476552 184078336 44076 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44941 44076 603 41 0 44900 0
vsize: 179764
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 27363
Raw data (stat): 27351 (minisat+) R 27350 20838 20837 0 -1 0 50314 0 0 0 119853 167 0 0 25 0 1 0 480476552 184991744 44293 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45164 44293 603 41 0 45123 0
vsize: 180656
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 27363
Raw data (stat): 27351 (minisat+) Z 27350 20838 20837 0 -1 12 50315 0 0 0 119853 177 0 0 25 0 1 0 480476552 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.14
CPU time (s): 1200.31
CPU user time (s): 1198.54
CPU system time (s): 1.77673
CPU usage (%): 100.015
Max. virtual memory (Kb): 180656
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####